:: TOPREAL2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: now
let x, X be set ; :: thesis: ( not x in X implies {x} /\ X = {} )
assume not x in X ; :: thesis: {x} /\ X = {}
then {x} misses X by ZFMISC_1:56;
hence {x} /\ X = {} by XBOOLE_0:def 7; :: thesis: verum
end;

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} )
proof end;

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} )
proof end;

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} )
proof end;

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} )
proof end;

theorem Th1: :: TOPREAL2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in R^2-unit_square & p2 in R^2-unit_square 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} )
proof end;

theorem Th2: :: TOPREAL2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
R^2-unit_square is compact
proof end;

theorem Th3: :: TOPREAL2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q1, q2 being Point of (TOP-REAL 2)
for Q, P being non empty Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | Q),((TOP-REAL 2) | P) st f is_homeomorphism & Q is_an_arc_of q1,q2 holds
for p1, p2 being Point of (TOP-REAL 2) st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2
proof end;

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

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

notation
let P be Subset of (TOP-REAL 2);
synonym P is_simple_closed_curve for being_simple_closed_curve P;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Subset of (TOP-REAL 2) st P is_simple_closed_curve holds
ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P )
proof end;

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_simple_closed_curve
proof end;

theorem Th5: :: TOPREAL2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Subset of (TOP-REAL 2) holds
( P is_simple_closed_curve iff ( ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) & ( for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P 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 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) ) ) )
proof end;

theorem :: TOPREAL2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Subset of (TOP-REAL 2) holds
( P is_simple_closed_curve iff ex p1, p2 being Point of (TOP-REAL 2) ex 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} ) )
proof end;

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
proof end;

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
proof end;

Lm30: for S, T being TopStruct st ex f being Function of S,T st f is_homeomorphism holds
( S is empty iff T 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;