:: TOPMETR3 semantic presentation

theorem Th1: :: TOPMETR3:1
for b1 being non empty Subset of REAL
for b2 being real number st ( for b3 being real number st b3 in b1 holds
b3 <= b2 ) holds
upper_bound b1 <= b2
proof end;

theorem Th2: :: TOPMETR3:2
for b1 being non empty MetrSpace
for b2 being sequence of b1
for b3 being Subset of (TopSpaceMetr b1) st b2 is convergent & ( for b4 being Nat holds b2 . b4 in b3 ) & b3 is closed holds
lim b2 in b3
proof end;

theorem Th3: :: TOPMETR3:3
for b1, b2 being non empty MetrSpace
for b3 being Function of (TopSpaceMetr b1),(TopSpaceMetr b2)
for b4 being sequence of b1 holds b3 * b4 is sequence of b2
proof end;

theorem Th4: :: TOPMETR3:4
for b1, b2 being non empty MetrSpace
for b3 being Function of (TopSpaceMetr b1),(TopSpaceMetr b2)
for b4 being sequence of b1
for b5 being sequence of b2 st b4 is convergent & b5 = b3 * b4 & b3 is continuous holds
b5 is convergent
proof end;

theorem Th5: :: TOPMETR3:5
canceled;

theorem Th6: :: TOPMETR3:6
for b1 being Real_Sequence
for b2 being sequence of RealSpace st b1 = b2 holds
( ( b1 is convergent implies b2 is convergent ) & ( b2 is convergent implies b1 is convergent ) & ( b1 is convergent implies lim b1 = lim b2 ) )
proof end;

theorem Th7: :: TOPMETR3:7
for b1, b2 being real number
for b3 being Real_Sequence st rng b3 c= [.b1,b2.] holds
b3 is sequence of (Closed-Interval-MSpace b1,b2)
proof end;

theorem Th8: :: TOPMETR3:8
for b1, b2 being real number
for b3 being sequence of (Closed-Interval-MSpace b1,b2) st b1 <= b2 holds
b3 is sequence of RealSpace
proof end;

theorem Th9: :: TOPMETR3:9
for b1, b2 being real number
for b3 being sequence of (Closed-Interval-MSpace b1,b2)
for b4 being sequence of RealSpace st b4 = b3 & b1 <= b2 holds
( ( b4 is convergent implies b3 is convergent ) & ( b3 is convergent implies b4 is convergent ) & ( b4 is convergent implies lim b4 = lim b3 ) )
proof end;

theorem Th10: :: TOPMETR3:10
for b1, b2 being real number
for b3 being Real_Sequence
for b4 being sequence of (Closed-Interval-MSpace b1,b2) st b4 = b3 & b1 <= b2 & b3 is convergent holds
( b4 is convergent & lim b3 = lim b4 )
proof end;

theorem Th11: :: TOPMETR3:11
for b1, b2 being real number
for b3 being Real_Sequence
for b4 being sequence of (Closed-Interval-MSpace b1,b2) st b4 = b3 & b1 <= b2 & b3 is non-decreasing holds
b4 is convergent
proof end;

theorem Th12: :: TOPMETR3:12
for b1, b2 being real number
for b3 being Real_Sequence
for b4 being sequence of (Closed-Interval-MSpace b1,b2) st b4 = b3 & b1 <= b2 & b3 is non-increasing holds
b4 is convergent
proof end;

theorem Th13: :: TOPMETR3:13
canceled;

theorem Th14: :: TOPMETR3:14
canceled;

theorem Th15: :: TOPMETR3:15
for b1 being non empty Subset of REAL st b1 is bounded_above holds
ex b2 being Real_Sequence st
( b2 is non-decreasing & b2 is convergent & rng b2 c= b1 & lim b2 = upper_bound b1 )
proof end;

theorem Th16: :: TOPMETR3:16
for b1 being non empty Subset of REAL st b1 is bounded_below holds
ex b2 being Real_Sequence st
( b2 is non-increasing & b2 is convergent & rng b2 c= b1 & lim b2 = lower_bound b1 )
proof end;

theorem Th17: :: TOPMETR3:17
for b1 being non empty MetrSpace
for b2 being Function of I[01] ,(TopSpaceMetr b1)
for b3, b4 being Subset of (TopSpaceMetr b1)
for b5, b6 being Real st 0 <= b5 & b6 <= 1 & b5 <= b6 & b2 . b5 in b3 & b2 . b6 in b4 & b3 is closed & b4 is closed & b2 is continuous & b3 \/ b4 = the carrier of b1 holds
ex b7 being Real st
( b5 <= b7 & b7 <= b6 & b2 . b7 in b3 /\ b4 )
proof end;

theorem Th18: :: TOPMETR3:18
for b1 being Nat
for b2, b3 being Point of (TOP-REAL b1)
for b4, b5 being non empty Subset of (TOP-REAL b1) st b4 is_an_arc_of b2,b3 & b5 is_an_arc_of b3,b2 & b5 c= b4 holds
b5 = b4
proof end;

theorem Th19: :: TOPMETR3:19
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 is_simple_closed_curve & b2 is_an_arc_of W-min b1, E-max b1 & b2 c= b1 & not b2 = Upper_Arc b1 holds
b2 = Lower_Arc b1
proof end;