reconsider RS = R^2-unit_square as non empty Subset of (TOP-REAL 2) ;
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 ) )
A1: |[0,0]| `1 = 0 by EUCLID:52;
A2: [#] ((TOP-REAL 2) | P) c= [#] (TOP-REAL 2) by PRE_TOPC:def 4;
A3: |[1,1]| `1 = 1 by EUCLID:52;
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
A4: f is being_homeomorphism ;
A5: rng f = [#] ((TOP-REAL 2) | P) by A4
.= P by PRE_TOPC:def 5 ;
reconsider f = f as Function of ((TOP-REAL 2) | RS),((TOP-REAL 2) | P) ;
A6: dom f = [#] ((TOP-REAL 2) | RS) by FUNCT_2:def 1
.= R^2-unit_square by PRE_TOPC:def 5 ;
set p1 = f . |[0,0]|;
set p2 = f . |[1,1]|;
|[0,0]| `2 = 0 by EUCLID:52;
then A7: |[0,0]| in dom f by A1, A6, TOPREAL1:14;
then A8: f . |[0,0]| in rng f by FUNCT_1:def 3;
|[1,1]| `2 = 1 by EUCLID:52;
then A9: |[1,1]| in dom f by A3, A6, TOPREAL1:14;
then A10: f . |[1,1]| in rng f by FUNCT_1:def 3;
reconsider p1 = f . |[0,0]|, p2 = f . |[1,1]| as Point of (TOP-REAL 2) by A2, A8, A10;
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 )
f is one-to-one by A4;
hence p1 <> p2 by A1, A3, A7, A9, FUNCT_1:def 4; :: thesis: ( p1 in P & p2 in P )
thus ( p1 in P & p2 in P ) by A5, A7, A9, FUNCT_1:def 3; :: thesis: verum