begin
:: deftheorem TOPREAL1:def 1 :
canceled;
:: deftheorem Def2 defines is_an_arc_of TOPREAL1:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem Th5:
definition
canceled;func R^2-unit_square -> Subset of
(TOP-REAL 2) equals
((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[1,1]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[0 ,0 ]|));
coherence
((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[1,1]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[0 ,0 ]|)) is Subset of (TOP-REAL 2)
;
end;
:: deftheorem TOPREAL1:def 3 :
canceled;
:: deftheorem defines R^2-unit_square TOPREAL1:def 4 :
R^2-unit_square = ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[1,1]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[0 ,0 ]|));
theorem
canceled;
theorem
canceled;
Lm1:
for n being Nat
for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg p1,p2 holds
LSeg p1,p c= LSeg p1,p2
theorem
canceled;
theorem
theorem
theorem Th11:
theorem Th12:
theorem
theorem
Lm2:
for T being TopSpace holds
( T is T_2 iff TopStruct(# the carrier of T,the topology of T #) is T_2 )
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
(
LSeg |[0 ,0 ]|,
|[0 ,1]| = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = 0 & p1 `2 <= 1 & p1 `2 >= 0 ) } &
LSeg |[0 ,1]|,
|[1,1]| = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } &
LSeg |[0 ,0 ]|,
|[1,0 ]| = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } &
LSeg |[1,0 ]|,
|[1,1]| = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } )
theorem
theorem
theorem
theorem Th23:
theorem Th24:
theorem
theorem Th26:
:: deftheorem Def5 defines LSeg TOPREAL1:def 5 :
theorem Th27:
:: deftheorem defines L~ TOPREAL1:def 6 :
theorem Th28:
theorem Th29:
:: deftheorem defines special TOPREAL1:def 7 :
:: deftheorem Def8 defines unfolded TOPREAL1:def 8 :
:: deftheorem Def9 defines s.n.c. TOPREAL1:def 9 :
:: deftheorem Def10 defines being_S-Seq TOPREAL1:def 10 :
theorem Th30:
theorem Th31:
:: deftheorem Def11 defines being_S-P_arc TOPREAL1:def 11 :
theorem Th32:
theorem
canceled;
theorem
theorem Th35:
theorem
:: deftheorem Def12 defines north_halfline TOPREAL1:def 12 :
:: deftheorem Def13 defines east_halfline TOPREAL1:def 13 :
:: deftheorem Def14 defines south_halfline TOPREAL1:def 14 :
:: deftheorem Def15 defines west_halfline TOPREAL1:def 15 :
theorem
theorem Th38:
theorem
theorem Th40:
theorem
theorem Th42:
theorem
theorem Th44:
theorem