:: The Topological Space ${\calE}^2_{\rm T}$. Simple Closed Curves
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received December 30, 1991
:: Copyright (c) 1991 Association of Mizar Users
Lm2:
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by TOPREAL1:25, XBOOLE_0:def 7;
Lm3:
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {}
by TOPREAL1:26, 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 & |[0 ,0 ]| `2 = 0 & |[0 ,1]| `1 = 0 & |[0 ,1]| `2 = 1 & |[1,0 ]| `1 = 1 & |[1,0 ]| `2 = 0 & |[1,1]| `1 = 1 & |[1,1]| `2 = 1 )
by EUCLID:56;
then Lm5:
not |[0 ,0 ]| in LSeg |[1,0 ]|,|[1,1]|
by TOPREAL1:9;
Lm6:
not |[0 ,0 ]| in LSeg |[0 ,1]|,|[1,1]|
by Lm4, TOPREAL1:10;
Lm7:
not |[0 ,1]| in LSeg |[0 ,0 ]|,|[1,0 ]|
by Lm4, TOPREAL1:10;
Lm8:
not |[0 ,1]| in LSeg |[1,0 ]|,|[1,1]|
by Lm4, TOPREAL1:9;
Lm9:
not |[1,0 ]| in LSeg |[0 ,0 ]|,|[0 ,1]|
by Lm4, TOPREAL1:9;
Lm10:
not |[1,0 ]| in LSeg |[0 ,1]|,|[1,1]|
by Lm4, TOPREAL1:10;
Lm11:
not |[1,1]| in LSeg |[0 ,0 ]|,|[0 ,1]|
by Lm4, TOPREAL1:9;
Lm12:
not |[1,1]| in LSeg |[0 ,0 ]|,|[1,0 ]|
by Lm4, TOPREAL1:10;
Lm13:
|[0 ,0 ]| in LSeg |[0 ,0 ]|,|[0 ,1]|
by TOPREAL1:6;
Lm14:
|[0 ,0 ]| in LSeg |[0 ,0 ]|,|[1,0 ]|
by TOPREAL1:6;
Lm15:
|[0 ,1]| in LSeg |[0 ,0 ]|,|[0 ,1]|
by TOPREAL1:6;
Lm16:
|[0 ,1]| in LSeg |[0 ,1]|,|[1,1]|
by TOPREAL1:6;
Lm17:
|[1,0 ]| in LSeg |[0 ,0 ]|,|[1,0 ]|
by TOPREAL1:6;
Lm18:
|[1,0 ]| in LSeg |[1,0 ]|,|[1,1]|
by TOPREAL1:6;
Lm19:
|[1,1]| in LSeg |[0 ,1]|,|[1,1]|
by TOPREAL1:6;
Lm20:
|[1,1]| in LSeg |[1,0 ]|,|[1,1]|
by TOPREAL1:6;
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 ) ) } ;
Lm21:
|[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;
Lm22:
|[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 Lm4;
Lm23:
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} )
Lm24:
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} )
Lm25:
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} )
Lm26:
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} )
theorem Th1: :: TOPREAL2:1
theorem Th2: :: TOPREAL2:2
theorem Th3: :: TOPREAL2:3
:: deftheorem Def1 defines being_simple_closed_curve TOPREAL2:def 1 :
theorem Th4: :: TOPREAL2:4
Lm27:
for p1, p2 being Point of (TOP-REAL 2)
for P, P1, P2 being non empty Subset of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P & 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
theorem Th5: :: TOPREAL2:5
theorem :: TOPREAL2:6
Lm28:
for S, T being 1-sorted
for f being Function of S,T st S is empty & rng f = [#] T holds
T is empty
Lm29:
for S, T being 1-sorted
for f being Function of S,T st T is empty & dom f = [#] S holds
S is empty
Lm30:
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 )