begin
Lm2:
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {}
by TOPREAL1:19, XBOOLE_0:def 7;
Lm3:
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
set p00 = |[0,0]|;
set p01 = |[0,1]|;
set p10 = |[1,0]|;
set p11 = |[1,1]|;
set L1 = LSeg (|[0,0]|,|[0,1]|);
set L2 = LSeg (|[0,1]|,|[1,1]|);
set L3 = LSeg (|[0,0]|,|[1,0]|);
set L4 = LSeg (|[1,0]|,|[1,1]|);
Lm4:
|[0,0]| `1 = 0
by EUCLID:52;
Lm5:
|[0,0]| `2 = 0
by EUCLID:52;
Lm6:
|[0,1]| `1 = 0
by EUCLID:52;
Lm7:
|[0,1]| `2 = 1
by EUCLID:52;
Lm8:
|[1,0]| `1 = 1
by EUCLID:52;
Lm9:
|[1,0]| `2 = 0
by EUCLID:52;
Lm10:
|[1,1]| `1 = 1
by EUCLID:52;
Lm11:
|[1,1]| `2 = 1
by EUCLID:52;
Lm12:
not |[0,0]| in LSeg (|[1,0]|,|[1,1]|)
by Lm4, Lm8, Lm10, TOPREAL1:3;
Lm13:
not |[0,0]| in LSeg (|[0,1]|,|[1,1]|)
by Lm5, Lm7, Lm11, TOPREAL1:4;
Lm14:
not |[0,1]| in LSeg (|[0,0]|,|[1,0]|)
by Lm5, Lm7, Lm9, TOPREAL1:4;
Lm15:
not |[0,1]| in LSeg (|[1,0]|,|[1,1]|)
by Lm6, Lm8, Lm10, TOPREAL1:3;
Lm16:
not |[1,0]| in LSeg (|[0,0]|,|[0,1]|)
by Lm4, Lm6, Lm8, TOPREAL1:3;
Lm17:
not |[1,0]| in LSeg (|[0,1]|,|[1,1]|)
by Lm7, Lm9, Lm11, TOPREAL1:4;
Lm18:
not |[1,1]| in LSeg (|[0,0]|,|[0,1]|)
by Lm4, Lm6, Lm10, TOPREAL1:3;
Lm19:
not |[1,1]| in LSeg (|[0,0]|,|[1,0]|)
by Lm5, Lm9, Lm11, TOPREAL1:4;
Lm20:
|[0,0]| in LSeg (|[0,0]|,|[0,1]|)
by RLTOPSP1:68;
Lm21:
|[0,0]| in LSeg (|[0,0]|,|[1,0]|)
by RLTOPSP1:68;
Lm22:
|[0,1]| in LSeg (|[0,0]|,|[0,1]|)
by RLTOPSP1:68;
Lm23:
|[0,1]| in LSeg (|[0,1]|,|[1,1]|)
by RLTOPSP1:68;
Lm24:
|[1,0]| in LSeg (|[0,0]|,|[1,0]|)
by RLTOPSP1:68;
Lm25:
|[1,0]| in LSeg (|[1,0]|,|[1,1]|)
by RLTOPSP1:68;
Lm26:
|[1,1]| in LSeg (|[0,1]|,|[1,1]|)
by RLTOPSP1:68;
Lm27:
|[1,1]| in LSeg (|[1,0]|,|[1,1]|)
by RLTOPSP1:68;
set L = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) or ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) ) } ;
Lm28:
|[0,0]| in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) or ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) ) }
by Lm4, Lm5;
Lm29:
|[1,1]| in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) or ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) ) }
by Lm10, Lm11;
Lm30:
for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (|[0,0]|,|[0,1]|) holds
ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
Lm31:
for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (|[0,1]|,|[1,1]|) holds
ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
Lm32:
for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (|[0,0]|,|[1,0]|) holds
ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
Lm33:
for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (|[1,0]|,|[1,1]|) holds
ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
Lm34:
for p1, p2 being Point of (TOP-REAL 2)
for P, P1, P2 being non empty Subset of (TOP-REAL 2) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} holds
P is being_simple_closed_curve
Lm35:
for S, T being 1-sorted
for f being Function of S,T st S is empty & rng f = [#] T holds
T is empty
Lm36:
for S, T being 1-sorted
for f being Function of S,T st T is empty & dom f = [#] S holds
S is empty
Lm37:
for S, T being TopStruct st ex f being Function of S,T st f is being_homeomorphism holds
( S is empty iff T is empty )