begin
definition
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 defines
R^2-unit_square TOPREAL1:def 2 :
R^2-unit_square = ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)));
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)
Lm2:
for T being TopSpace holds
( T is T_2 iff TopStruct(# the carrier of T, the topology of T #) is T_2 )
theorem Th13:
(
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 ) } )