:: TOPREALA semantic presentation

set c1 = the carrier of R^1 ;

Lemma1: the carrier of [:R^1 ,R^1 :] = [:the carrier of R^1 ,the carrier of R^1 :]
by BORSUK_1:def 5;

reconsider c2 = 1 as real positive number ;

theorem Th1: :: TOPREALA:1
for b1 being Integer
for b2 being real number holds frac (b2 + b1) = frac b2
proof end;

theorem Th2: :: TOPREALA:2
for b1, b2 being real number st b1 <= b2 & b2 < [\b1/] + 1 holds
[\b2/] = [\b1/]
proof end;

theorem Th3: :: TOPREALA:3
for b1, b2 being real number st b1 <= b2 & b2 < [\b1/] + 1 holds
frac b1 <= frac b2
proof end;

theorem Th4: :: TOPREALA:4
for b1, b2 being real number st b1 < b2 & b2 < [\b1/] + 1 holds
frac b1 < frac b2
proof end;

theorem Th5: :: TOPREALA:5
for b1, b2 being real number st b1 >= [\b2/] + 1 & b1 <= b2 + 1 holds
[\b1/] = [\b2/] + 1
proof end;

theorem Th6: :: TOPREALA:6
for b1, b2 being real number st b1 >= [\b2/] + 1 & b1 < b2 + 1 holds
frac b1 < frac b2
proof end;

theorem Th7: :: TOPREALA:7
for b1, b2, b3 being real number st b1 <= b2 & b2 < b1 + 1 & b1 <= b3 & b3 < b1 + 1 & frac b2 = frac b3 holds
b2 = b3
proof end;

registration
let c3 be real number ;
let c4 be real positive number ;
cluster ].a1,(a1 + a2).[ -> non empty ;
coherence
not ].c3,(c3 + c4).[ is empty
proof end;
cluster [.a1,(a1 + a2).[ -> non empty ;
coherence
not [.c3,(c3 + c4).[ is empty
proof end;
cluster ].a1,(a1 + a2).] -> non empty ;
coherence
not ].c3,(c3 + c4).] is empty
proof end;
cluster [.a1,(a1 + a2).] -> non empty ;
coherence
not [.c3,(c3 + c4).] is empty
proof end;
cluster ].(a1 - a2),a1.[ -> non empty ;
coherence
not ].(c3 - c4),c3.[ is empty
proof end;
cluster [.(a1 - a2),a1.[ -> non empty ;
coherence
not [.(c3 - c4),c3.[ is empty
proof end;
cluster ].(a1 - a2),a1.] -> non empty ;
coherence
not ].(c3 - c4),c3.] is empty
proof end;
cluster [.(a1 - a2),a1.] -> non empty ;
coherence
not [.(c3 - c4),c3.] is empty
proof end;
end;

registration
let c3 be real non positive number ;
let c4 be real positive number ;
cluster ].a1,a2.[ -> non empty ;
coherence
not ].c3,c4.[ is empty
proof end;
cluster [.a1,a2.[ -> non empty ;
coherence
not [.c3,c4.[ is empty by RCOMP_2:3;
cluster ].a1,a2.] -> non empty ;
coherence
not ].c3,c4.] is empty by RCOMP_2:4;
cluster [.a1,a2.] -> non empty ;
coherence
not [.c3,c4.] is empty by RCOMP_1:48;
end;

registration
let c3 be real negative number ;
let c4 be real non negative number ;
cluster ].a1,a2.[ -> non empty ;
coherence
not ].c3,c4.[ is empty
proof end;
cluster [.a1,a2.[ -> non empty ;
coherence
not [.c3,c4.[ is empty by RCOMP_2:3;
cluster ].a1,a2.] -> non empty ;
coherence
not ].c3,c4.] is empty by RCOMP_2:4;
cluster [.a1,a2.] -> non empty ;
coherence
not [.c3,c4.] is empty by RCOMP_1:48;
end;

theorem Th8: :: TOPREALA:8
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 < b4 holds
[.b2,b3.] c= [.b1,b4.[
proof end;

theorem Th9: :: TOPREALA:9
for b1, b2, b3, b4 being real number st b1 < b2 & b3 <= b4 holds
[.b2,b3.] c= ].b1,b4.]
proof end;

theorem Th10: :: TOPREALA:10
for b1, b2, b3, b4 being real number st b1 < b2 & b3 < b4 holds
[.b2,b3.] c= ].b1,b4.[
proof end;

theorem Th11: :: TOPREALA:11
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
[.b2,b3.[ c= [.b1,b4.]
proof end;

theorem Th12: :: TOPREALA:12
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
[.b2,b3.[ c= [.b1,b4.[
proof end;

theorem Th13: :: TOPREALA:13
for b1, b2, b3, b4 being real number st b1 < b2 & b3 <= b4 holds
[.b2,b3.[ c= ].b1,b4.]
proof end;

theorem Th14: :: TOPREALA:14
for b1, b2, b3, b4 being real number st b1 < b2 & b3 <= b4 holds
[.b2,b3.[ c= ].b1,b4.[
proof end;

theorem Th15: :: TOPREALA:15
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
].b2,b3.] c= [.b1,b4.]
proof end;

theorem Th16: :: TOPREALA:16
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 < b4 holds
].b2,b3.] c= [.b1,b4.[
proof end;

theorem Th17: :: TOPREALA:17
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
].b2,b3.] c= ].b1,b4.]
proof end;

theorem Th18: :: TOPREALA:18
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 < b4 holds
].b2,b3.] c= ].b1,b4.[
proof end;

theorem Th19: :: TOPREALA:19
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
].b2,b3.[ c= [.b1,b4.]
proof end;

theorem Th20: :: TOPREALA:20
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
].b2,b3.[ c= [.b1,b4.[
proof end;

theorem Th21: :: TOPREALA:21
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
].b2,b3.[ c= ].b1,b4.]
proof end;

theorem Th22: :: TOPREALA:22
for b1 being Function
for b2, b3 being set st b2 in dom b1 & b1 . b2 in b1 .: b3 & b1 is one-to-one holds
b2 in b3
proof end;

theorem Th23: :: TOPREALA:23
for b1 being FinSequence
for b2 being natural number holds
( not b2 + 1 in dom b1 or b2 in dom b1 or b2 = 0 )
proof end;

theorem Th24: :: TOPREALA:24
for b1, b2, b3, b4 being set
for b5 being Function st b1 <> b2 & b5 in product (b1,b2 --> b3,b4) holds
( b5 . b1 in b3 & b5 . b2 in b4 )
proof end;

theorem Th25: :: TOPREALA:25
for b1, b2 being set holds <*b1,b2*> = 1,2 --> b1,b2
proof end;

registration
cluster non empty strict constituted-FinSeqs TopStruct ;
existence
ex b1 being TopSpace st
( b1 is constituted-FinSeqs & not b1 is empty & b1 is strict )
proof end;
end;

registration
let c3 be constituted-FinSeqs TopSpace;
cluster -> constituted-FinSeqs SubSpace of a1;
coherence
for b1 being SubSpace of c3 holds b1 is constituted-FinSeqs
proof end;
end;

theorem Th26: :: TOPREALA:26
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3 being Point of b1
for b4 being Point of b2
for b5 being open a_neighborhood of b3
for b6 being Subset of b2 st b3 = b4 & b6 = b5 /\ ([#] b2) holds
b6 is open a_neighborhood of b4
proof end;

registration
cluster empty -> discrete anti-discrete TopStruct ;
coherence
for b1 being TopSpace st b1 is empty holds
( b1 is discrete & b1 is anti-discrete )
proof end;
end;

registration
let c3 be discrete TopSpace;
let c4 be TopSpace;
cluster -> continuous Relation of the carrier of a1,the carrier of a2;
coherence
for b1 being Function of c3,c4 holds b1 is continuous by TEX_2:68;
end;

theorem Th27: :: TOPREALA:27
for b1 being TopSpace
for b2 being TopStruct
for b3 being Function of b1,b2 st b3 is empty holds
b3 is continuous
proof end;

registration
let c3 be TopSpace;
let c4 be TopStruct ;
cluster empty -> continuous Relation of the carrier of a1,the carrier of a2;
coherence
for b1 being Function of c3,c4 st b1 is empty holds
b1 is continuous by Th27;
end;

theorem Th28: :: TOPREALA:28
for b1 being TopStruct
for b2 being non empty TopStruct
for b3 being non empty SubSpace of b2
for b4 being Function of b1,b3 holds b4 is Function of b1,b2
proof end;

theorem Th29: :: TOPREALA:29
for b1, b2 being non empty TopSpace
for b3 being Subset of b1
for b4 being Subset of b2
for b5 being continuous Function of b1,b2
for b6 being Function of (b1 | b3),(b2 | b4) st b6 = b5 | b3 holds
b6 is continuous
proof end;

theorem Th30: :: TOPREALA:30
for b1, b2 being non empty TopSpace
for b3 being non empty SubSpace of b2
for b4 being Function of b1,b2
for b5 being Function of b1,b3 st b4 = b5 & b4 is open holds
b5 is open
proof end;

theorem Th31: :: TOPREALA:31
for b1, b2 being non empty TopSpace
for b3 being Subset of b1
for b4 being Subset of b2
for b5 being Function of b1,b2
for b6 being Function of (b1 | b3),(b2 | b4) st b6 = b5 | b3 & b6 is onto & b5 is open & b5 is one-to-one holds
b6 is open
proof end;

theorem Th32: :: TOPREALA:32
for b1, b2, b3 being non empty TopSpace
for b4 being Function of b1,b2
for b5 being Function of b2,b3 st b4 is open & b5 is open holds
b5 * b4 is open
proof end;

theorem Th33: :: TOPREALA:33
for b1, b2 being TopSpace
for b3 being open SubSpace of b2
for b4 being Function of b1,b2
for b5 being Function of b1,b3 st b4 = b5 & b5 is open holds
b4 is open
proof end;

theorem Th34: :: TOPREALA:34
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 st b3 is one-to-one & b3 is onto holds
( b3 is continuous iff b3 " is open )
proof end;

theorem Th35: :: TOPREALA:35
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 st b3 is one-to-one & b3 is onto holds
( b3 is open iff b3 " is continuous )
proof end;

theorem Th36: :: TOPREALA:36
for b1 being TopSpace
for b2 being non empty TopSpace holds
( b1,b2 are_homeomorphic iff TopStruct(# the carrier of b1,the topology of b1 #), TopStruct(# the carrier of b2,the topology of b2 #) are_homeomorphic )
proof end;

theorem Th37: :: TOPREALA:37
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 st b3 is one-to-one & b3 is onto & b3 is continuous & b3 is open holds
b3 is_homeomorphism
proof end;

theorem Th38: :: TOPREALA:38
for b1 being real number
for b2 being PartFunc of REAL , REAL st b2 = REAL --> b1 holds
b2 is_continuous_on REAL
proof end;

theorem Th39: :: TOPREALA:39
for b1, b2, b3 being PartFunc of REAL , REAL st dom b1 = (dom b2) \/ (dom b3) & dom b2 is open & dom b3 is open & b2 is_continuous_on dom b2 & b3 is_continuous_on dom b3 & ( for b4 being set st b4 in dom b2 holds
b1 . b4 = b2 . b4 ) & ( for b4 being set st b4 in dom b3 holds
b1 . b4 = b3 . b4 ) holds
b1 is_continuous_on dom b1
proof end;

theorem Th40: :: TOPREALA:40
for b1 being Point of R^1
for b2 being Subset of REAL
for b3 being Subset of R^1 st b3 = b2 & b2 is Neighbourhood of b1 holds
b3 is a_neighborhood of b1
proof end;

theorem Th41: :: TOPREALA:41
for b1 being Point of R^1
for b2 being a_neighborhood of b1 ex b3 being Neighbourhood of b1 st b3 c= b2
proof end;

theorem Th42: :: TOPREALA:42
for b1 being Function of R^1 ,R^1
for b2 being PartFunc of REAL , REAL
for b3 being Point of R^1 st b1 = b2 & b2 is_continuous_in b3 holds
b1 is_continuous_at b3
proof end;

theorem Th43: :: TOPREALA:43
for b1 being Function of R^1 ,R^1
for b2 being Function of REAL , REAL st b1 = b2 & b2 is_continuous_on REAL holds
b1 is continuous
proof end;

theorem Th44: :: TOPREALA:44
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
[.b2,b3.] is closed Subset of (Closed-Interval-TSpace b1,b4)
proof end;

theorem Th45: :: TOPREALA:45
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
].b2,b3.[ is open Subset of (Closed-Interval-TSpace b1,b4)
proof end;

theorem Th46: :: TOPREALA:46
for b1, b2, b3 being real number st b1 <= b2 & b1 <= b3 holds
].b3,b2.] is open Subset of (Closed-Interval-TSpace b1,b2)
proof end;

theorem Th47: :: TOPREALA:47
for b1, b2, b3 being real number st b1 <= b2 & b3 <= b2 holds
[.b1,b3.[ is open Subset of (Closed-Interval-TSpace b1,b2)
proof end;

theorem Th48: :: TOPREALA:48
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
the carrier of [:(Closed-Interval-TSpace b1,b2),(Closed-Interval-TSpace b3,b4):] = [:[.b1,b2.],[.b3,b4.]:]
proof end;

theorem Th49: :: TOPREALA:49
for b1, b2 being real number holds |[b1,b2]| = 1,2 --> b1,b2
proof end;

theorem Th50: :: TOPREALA:50
for b1, b2 being real number holds
( |[b1,b2]| . 1 = b1 & |[b1,b2]| . 2 = b2 )
proof end;

theorem Th51: :: TOPREALA:51
for b1, b2, b3, b4 being real number holds closed_inside_of_rectangle b1,b2,b3,b4 = product (1,2 --> [.b1,b2.],[.b3,b4.])
proof end;

theorem Th52: :: TOPREALA:52
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
|[b1,b3]| in closed_inside_of_rectangle b1,b2,b3,b4
proof end;

definition
let c3, c4, c5, c6 be real number ;
func Trectangle c1,c2,c3,c4 -> SubSpace of TOP-REAL 2 equals :: TOPREALA:def 1
(TOP-REAL 2) | (closed_inside_of_rectangle a1,a2,a3,a4);
coherence
(TOP-REAL 2) | (closed_inside_of_rectangle c3,c4,c5,c6) is SubSpace of TOP-REAL 2 ;
end;

:: deftheorem Def1 defines Trectangle TOPREALA:def 1 :
for b1, b2, b3, b4 being real number holds Trectangle b1,b2,b3,b4 = (TOP-REAL 2) | (closed_inside_of_rectangle b1,b2,b3,b4);

theorem Th53: :: TOPREALA:53
for b1, b2, b3, b4 being real number holds the carrier of (Trectangle b1,b2,b3,b4) = closed_inside_of_rectangle b1,b2,b3,b4 by JORDAN1:1;

theorem Th54: :: TOPREALA:54
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
not Trectangle b1,b2,b3,b4 is empty
proof end;

registration
let c3, c4 be real non positive number ;
let c5, c6 be real non negative number ;
cluster Trectangle a1,a3,a2,a4 -> non empty constituted-FinSeqs ;
coherence
not Trectangle c3,c5,c4,c6 is empty by Th54;
end;

definition
func R2Homeomorphism -> Function of [:R^1 ,R^1 :],(TOP-REAL 2) means :Def2: :: TOPREALA:def 2
for b1, b2 being real number holds a1 . [b1,b2] = <*b1,b2*>;
existence
ex b1 being Function of [:R^1 ,R^1 :],(TOP-REAL 2) st
for b2, b3 being real number holds b1 . [b2,b3] = <*b2,b3*>
proof end;
uniqueness
for b1, b2 being Function of [:R^1 ,R^1 :],(TOP-REAL 2) st ( for b3, b4 being real number holds b1 . [b3,b4] = <*b3,b4*> ) & ( for b3, b4 being real number holds b2 . [b3,b4] = <*b3,b4*> ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines R2Homeomorphism TOPREALA:def 2 :
for b1 being Function of [:R^1 ,R^1 :],(TOP-REAL 2) holds
( b1 = R2Homeomorphism iff for b2, b3 being real number holds b1 . [b2,b3] = <*b2,b3*> );

theorem Th55: :: TOPREALA:55
for b1, b2 being Subset of REAL holds R2Homeomorphism .: [:b1,b2:] = product (1,2 --> b1,b2)
proof end;

theorem Th56: :: TOPREALA:56
R2Homeomorphism is_homeomorphism
proof end;

theorem Th57: :: TOPREALA:57
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace b1,b2),(Closed-Interval-TSpace b3,b4):] is Function of [:(Closed-Interval-TSpace b1,b2),(Closed-Interval-TSpace b3,b4):],(Trectangle b1,b2,b3,b4)
proof end;

theorem Th58: :: TOPREALA:58
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
for b5 being Function of [:(Closed-Interval-TSpace b1,b2),(Closed-Interval-TSpace b3,b4):],(Trectangle b1,b2,b3,b4) st b5 = R2Homeomorphism | the carrier of [:(Closed-Interval-TSpace b1,b2),(Closed-Interval-TSpace b3,b4):] holds
b5 is_homeomorphism
proof end;

theorem Th59: :: TOPREALA:59
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
[:(Closed-Interval-TSpace b1,b2),(Closed-Interval-TSpace b3,b4):], Trectangle b1,b2,b3,b4 are_homeomorphic
proof end;

theorem Th60: :: TOPREALA:60
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
for b5 being Subset of (Closed-Interval-TSpace b1,b2)
for b6 being Subset of (Closed-Interval-TSpace b3,b4) holds product (1,2 --> b5,b6) is Subset of (Trectangle b1,b2,b3,b4)
proof end;

theorem Th61: :: TOPREALA:61
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
for b5 being open Subset of (Closed-Interval-TSpace b1,b2)
for b6 being open Subset of (Closed-Interval-TSpace b3,b4) holds product (1,2 --> b5,b6) is open Subset of (Trectangle b1,b2,b3,b4)
proof end;

theorem Th62: :: TOPREALA:62
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
for b5 being closed Subset of (Closed-Interval-TSpace b1,b2)
for b6 being closed Subset of (Closed-Interval-TSpace b3,b4) holds product (1,2 --> b5,b6) is closed Subset of (Trectangle b1,b2,b3,b4)
proof end;