:: TOPREAL2 semantic presentation

E1: now
let c1, c2 be set ;
assume not c1 in c2 ;
then {c1} misses c2 by ZFMISC_1:56;
hence {c1} /\ c2 = {} by XBOOLE_0:def 7;
end;

Lemma2: (LSeg |[0,0]|,|[1,0]|) /\ (LSeg |[0,1]|,|[1,1]|) = {}
by TOPREAL1:25, XBOOLE_0:def 7;

Lemma3: (LSeg |[0,0]|,|[0,1]|) /\ (LSeg |[1,0]|,|[1,1]|) = {}
by TOPREAL1:26, XBOOLE_0:def 7;

set c1 = |[0,0]|;

set c2 = |[0,1]|;

set c3 = |[1,0]|;

set c4 = |[1,1]|;

set c5 = LSeg |[0,0]|,|[0,1]|;

set c6 = LSeg |[0,1]|,|[1,1]|;

set c7 = LSeg |[0,0]|,|[1,0]|;

set c8 = LSeg |[1,0]|,|[1,1]|;

Lemma4: ( |[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 Lemma5: not |[0,0]| in LSeg |[1,0]|,|[1,1]|
by TOPREAL1:9;

Lemma6: not |[0,0]| in LSeg |[0,1]|,|[1,1]|
by Lemma4, TOPREAL1:10;

Lemma7: not |[0,1]| in LSeg |[0,0]|,|[1,0]|
by Lemma4, TOPREAL1:10;

Lemma8: not |[0,1]| in LSeg |[1,0]|,|[1,1]|
by Lemma4, TOPREAL1:9;

Lemma9: not |[1,0]| in LSeg |[0,0]|,|[0,1]|
by Lemma4, TOPREAL1:9;

Lemma10: not |[1,0]| in LSeg |[0,1]|,|[1,1]|
by Lemma4, TOPREAL1:10;

Lemma11: not |[1,1]| in LSeg |[0,0]|,|[0,1]|
by Lemma4, TOPREAL1:9;

Lemma12: not |[1,1]| in LSeg |[0,0]|,|[1,0]|
by Lemma4, TOPREAL1:10;

Lemma13: |[0,0]| in LSeg |[0,0]|,|[0,1]|
by TOPREAL1:6;

Lemma14: |[0,0]| in LSeg |[0,0]|,|[1,0]|
by TOPREAL1:6;

Lemma15: |[0,1]| in LSeg |[0,0]|,|[0,1]|
by TOPREAL1:6;

Lemma16: |[0,1]| in LSeg |[0,1]|,|[1,1]|
by TOPREAL1:6;

Lemma17: |[1,0]| in LSeg |[0,0]|,|[1,0]|
by TOPREAL1:6;

Lemma18: |[1,0]| in LSeg |[1,0]|,|[1,1]|
by TOPREAL1:6;

Lemma19: |[1,1]| in LSeg |[0,1]|,|[1,1]|
by TOPREAL1:6;

Lemma20: |[1,1]| in LSeg |[1,0]|,|[1,1]|
by TOPREAL1:6;

set c9 = { b1 where B is Point of (TOP-REAL 2) : ( ( b1 `1 = 0 & b1 `2 <= 1 & b1 `2 >= 0 ) or ( b1 `1 <= 1 & b1 `1 >= 0 & b1 `2 = 1 ) or ( b1 `1 <= 1 & b1 `1 >= 0 & b1 `2 = 0 ) or ( b1 `1 = 1 & b1 `2 <= 1 & b1 `2 >= 0 ) ) } ;

Lemma21: |[0,0]| in { b1 where B is Point of (TOP-REAL 2) : ( ( b1 `1 = 0 & b1 `2 <= 1 & b1 `2 >= 0 ) or ( b1 `1 <= 1 & b1 `1 >= 0 & b1 `2 = 1 ) or ( b1 `1 <= 1 & b1 `1 >= 0 & b1 `2 = 0 ) or ( b1 `1 = 1 & b1 `2 <= 1 & b1 `2 >= 0 ) ) }
by Lemma4;

Lemma22: |[1,1]| in { b1 where B is Point of (TOP-REAL 2) : ( ( b1 `1 = 0 & b1 `2 <= 1 & b1 `2 >= 0 ) or ( b1 `1 <= 1 & b1 `1 >= 0 & b1 `2 = 1 ) or ( b1 `1 <= 1 & b1 `1 >= 0 & b1 `2 = 0 ) or ( b1 `1 = 1 & b1 `2 <= 1 & b1 `2 >= 0 ) ) }
by Lemma4;

Lemma23: for b1, b2 being Point of (TOP-REAL 2) st b1 <> b2 & b2 in R^2-unit_square & b1 in LSeg |[0,0]|,|[0,1]| holds
ex b3, b4 being non empty Subset of (TOP-REAL 2) st
( b3 is_an_arc_of b1,b2 & b4 is_an_arc_of b1,b2 & R^2-unit_square = b3 \/ b4 & b3 /\ b4 = {b1,b2} )
proof end;

Lemma24: for b1, b2 being Point of (TOP-REAL 2) st b1 <> b2 & b2 in R^2-unit_square & b1 in LSeg |[0,1]|,|[1,1]| holds
ex b3, b4 being non empty Subset of (TOP-REAL 2) st
( b3 is_an_arc_of b1,b2 & b4 is_an_arc_of b1,b2 & R^2-unit_square = b3 \/ b4 & b3 /\ b4 = {b1,b2} )
proof end;

Lemma25: for b1, b2 being Point of (TOP-REAL 2) st b1 <> b2 & b2 in R^2-unit_square & b1 in LSeg |[0,0]|,|[1,0]| holds
ex b3, b4 being non empty Subset of (TOP-REAL 2) st
( b3 is_an_arc_of b1,b2 & b4 is_an_arc_of b1,b2 & R^2-unit_square = b3 \/ b4 & b3 /\ b4 = {b1,b2} )
proof end;

Lemma26: for b1, b2 being Point of (TOP-REAL 2) st b1 <> b2 & b2 in R^2-unit_square & b1 in LSeg |[1,0]|,|[1,1]| holds
ex b3, b4 being non empty Subset of (TOP-REAL 2) st
( b3 is_an_arc_of b1,b2 & b4 is_an_arc_of b1,b2 & R^2-unit_square = b3 \/ b4 & b3 /\ b4 = {b1,b2} )
proof end;

theorem Th1: :: TOPREAL2:1
for b1, b2 being Point of (TOP-REAL 2) st b1 <> b2 & b1 in R^2-unit_square & b2 in R^2-unit_square holds
ex b3, b4 being non empty Subset of (TOP-REAL 2) st
( b3 is_an_arc_of b1,b2 & b4 is_an_arc_of b1,b2 & R^2-unit_square = b3 \/ b4 & b3 /\ b4 = {b1,b2} )
proof end;

theorem Th2: :: TOPREAL2:2
R^2-unit_square is compact
proof end;

theorem Th3: :: TOPREAL2:3
for b1, b2 being Point of (TOP-REAL 2)
for b3, b4 being non empty Subset of (TOP-REAL 2)
for b5 being Function of ((TOP-REAL 2) | b3),((TOP-REAL 2) | b4) st b5 is_homeomorphism & b3 is_an_arc_of b1,b2 holds
for b6, b7 being Point of (TOP-REAL 2) st b6 = b5 . b1 & b7 = b5 . b2 holds
b4 is_an_arc_of b6,b7
proof end;

definition
let c10 be Subset of (TOP-REAL 2);
attr a1 is being_simple_closed_curve means :Def1: :: TOPREAL2:def 1
ex b1 being Function of ((TOP-REAL 2) | R^2-unit_square ),((TOP-REAL 2) | a1) st b1 is_homeomorphism ;
end;

:: deftheorem Def1 defines being_simple_closed_curve TOPREAL2:def 1 :
for b1 being Subset of (TOP-REAL 2) holds
( b1 is being_simple_closed_curve iff ex b2 being Function of ((TOP-REAL 2) | R^2-unit_square ),((TOP-REAL 2) | b1) st b2 is_homeomorphism );

notation
let c10 be Subset of (TOP-REAL 2);
synonym c1 is_simple_closed_curve for being_simple_closed_curve c1;
end;

registration
cluster R^2-unit_square -> being_simple_closed_curve ;
coherence
R^2-unit_square is being_simple_closed_curve
proof end;
end;

registration
cluster being_simple_closed_curve Element of K22(the carrier of (TOP-REAL 2));
existence
ex b1 being Subset of (TOP-REAL 2) st b1 is being_simple_closed_curve
proof end;
end;

definition
mode Simple_closed_curve is being_simple_closed_curve Subset of (TOP-REAL 2);
end;

theorem Th4: :: TOPREAL2:4
for b1 being non empty Subset of (TOP-REAL 2) st b1 is_simple_closed_curve holds
ex b2, b3 being Point of (TOP-REAL 2) st
( b2 <> b3 & b2 in b1 & b3 in b1 )
proof end;

Lemma32: for b1, b2 being Point of (TOP-REAL 2)
for b3, b4, b5 being non empty Subset of (TOP-REAL 2) st b1 <> b2 & b1 in b3 & b2 in b3 & b4 is_an_arc_of b1,b2 & b5 is_an_arc_of b1,b2 & b3 = b4 \/ b5 & b4 /\ b5 = {b1,b2} holds
b3 is_simple_closed_curve
proof end;

theorem Th5: :: TOPREAL2:5
for b1 being non empty Subset of (TOP-REAL 2) holds
( b1 is_simple_closed_curve iff ( ex b2, b3 being Point of (TOP-REAL 2) st
( b2 <> b3 & b2 in b1 & b3 in b1 ) & ( for b2, b3 being Point of (TOP-REAL 2) st b2 <> b3 & b2 in b1 & b3 in b1 holds
ex b4, b5 being non empty Subset of (TOP-REAL 2) st
( b4 is_an_arc_of b2,b3 & b5 is_an_arc_of b2,b3 & b1 = b4 \/ b5 & b4 /\ b5 = {b2,b3} ) ) ) )
proof end;

theorem Th6: :: TOPREAL2:6
for b1 being non empty Subset of (TOP-REAL 2) holds
( b1 is_simple_closed_curve iff ex b2, b3 being Point of (TOP-REAL 2)ex b4, b5 being non empty Subset of (TOP-REAL 2) st
( b2 <> b3 & b2 in b1 & b3 in b1 & b4 is_an_arc_of b2,b3 & b5 is_an_arc_of b2,b3 & b1 = b4 \/ b5 & b4 /\ b5 = {b2,b3} ) )
proof end;

Lemma34: for b1, b2 being 1-sorted
for b3 being Function of b1,b2 st b1 is empty & rng b3 = [#] b2 holds
b2 is empty
proof end;

Lemma35: for b1, b2 being 1-sorted
for b3 being Function of b1,b2 st b2 is empty & dom b3 = [#] b1 holds
b1 is empty
proof end;

Lemma36: for b1, b2 being TopStruct st ex b3 being Function of b1,b2 st b3 is_homeomorphism holds
( b1 is empty iff b2 is empty )
proof end;

registration
cluster being_simple_closed_curve -> non empty compact Element of K22(the carrier of (TOP-REAL 2));
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is being_simple_closed_curve holds
( not b1 is empty & b1 is compact )
proof end;
end;