:: by Agata Darmochwa{\l} and Yatsuka Nakamura

::

:: Received December 30, 1991

:: Copyright (c) 1991-2012 Association of Mizar Users

begin

Lm1: now :: thesis: for x, X being set st not x in X holds

{x} /\ X = {}

{x} /\ X = {}

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:50;

hence {x} /\ X = {} by XBOOLE_0:def 7; :: thesis: verum

end;
assume not x in X ; :: thesis: {x} /\ X = {}

then {x} misses X by ZFMISC_1:50;

hence {x} /\ X = {} by XBOOLE_0:def 7; :: thesis: verum

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} )

proof end;

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} )

proof end;

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} )

proof end;

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} )

proof end;

theorem Th1: :: TOPREAL2:1

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} )

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 Th3: :: TOPREAL2:3

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 being_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

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 being_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);

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

ex f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) st f is being_homeomorphism ;

:: 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 being_homeomorphism );

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 being_homeomorphism );

registration

ex b_{1} being Subset of (TOP-REAL 2) st

( b_{1} is being_simple_closed_curve & not b_{1} is empty )
end;

cluster functional non empty being_simple_closed_curve for Element of K19( the carrier of (TOP-REAL 2));

existence ex b

( b

proof end;

theorem Th4: :: TOPREAL2:4

for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds

ex p1, p2 being Point of (TOP-REAL 2) st

( p1 <> p2 & p1 in P & p2 in P )

ex p1, p2 being Point of (TOP-REAL 2) st

( p1 <> p2 & p1 in P & p2 in P )

proof end;

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

proof end;

theorem Th5: :: TOPREAL2:5

for P being non empty Subset of (TOP-REAL 2) holds

( P is being_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} ) ) ) )

( P is being_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

for P being non empty Subset of (TOP-REAL 2) holds

( P is being_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} ) )

( P is being_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;

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

proof end;

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

proof end;

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 )

proof end;

registration

for b_{1} being Subset of (TOP-REAL 2) st b_{1} is being_simple_closed_curve holds

( not b_{1} is empty & b_{1} is compact )
end;

cluster being_simple_closed_curve -> non empty compact for Element of K19( the carrier of (TOP-REAL 2));

coherence for b

( not b

proof end;