let P be non empty Subset of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve implies ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P ) )
assume P is being_simple_closed_curve ; :: thesis: ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P )
then consider f being Function of ((TOP-REAL 2) | R^2-unit_square ),((TOP-REAL 2) | P) such that
A1: f is being_homeomorphism by Def1;
A2: rng f = [#] ((TOP-REAL 2) | P) by A1, TOPS_2:def 5
.= P by PRE_TOPC:def 10 ;
A3: ( |[0 ,0 ]| `1 = 0 & |[0 ,0 ]| `2 = 0 & |[1,1]| `1 = 1 & |[1,1]| `2 = 1 ) by EUCLID:56;
reconsider RS = R^2-unit_square as non empty Subset of (TOP-REAL 2) ;
reconsider f = f as Function of ((TOP-REAL 2) | RS),((TOP-REAL 2) | P) ;
dom f = [#] ((TOP-REAL 2) | RS) by FUNCT_2:def 1
.= R^2-unit_square by PRE_TOPC:def 10 ;
then A4: ( |[0 ,0 ]| in dom f & |[1,1]| in dom f ) by A3, TOPREAL1:20;
set p1 = f . |[0 ,0 ]|;
set p2 = f . |[1,1]|;
( rng f = [#] ((TOP-REAL 2) | P) & [#] ((TOP-REAL 2) | P) c= [#] (TOP-REAL 2) & f . |[0 ,0 ]| in rng f & f . |[1,1]| in rng f ) by A1, A4, FUNCT_1:def 5, PRE_TOPC:def 9, TOPS_2:def 5;
then reconsider p1 = f . |[0 ,0 ]|, p2 = f . |[1,1]| as Point of (TOP-REAL 2) ;
take p1 ; :: thesis: ex p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P )
take p2 ; :: thesis: ( p1 <> p2 & p1 in P & p2 in P )
( |[0 ,0 ]| <> |[1,1]| & f is one-to-one ) by A1, A3, TOPS_2:def 5;
hence p1 <> p2 by A4, FUNCT_1:def 8; :: thesis: ( p1 in P & p2 in P )
thus ( p1 in P & p2 in P ) by A2, A4, FUNCT_1:def 5; :: thesis: verum