reconsider RS = R^2-unit_square as non empty Subset of () ;
let P be non empty Subset of (); :: thesis: ( P is being_simple_closed_curve implies ex p1, p2 being Point of () st
( p1 <> p2 & p1 in P & p2 in P ) )

A1: |[0,0]| `1 = 0 by EUCLID:52;
A2: [#] (() | P) c= [#] () 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 () st
( p1 <> p2 & p1 in P & p2 in P )

then consider f being Function of (),(() | P) such that
A4: f is being_homeomorphism ;
A5: rng f = [#] (() | P) by A4
.= P by PRE_TOPC:def 5 ;
reconsider f = f as Function of (() | RS),(() | P) ;
A6: dom f = [#] (() | RS) by FUNCT_2:def 1
.= R^2-unit_square by PRE_TOPC:def 5 ;
set p1 = f . ;
set p2 = f . |[1,1]|;
|[0,0]| `2 = 0 by EUCLID:52;
then A7: |[0,0]| in dom f by ;
then A8: f . in rng f by FUNCT_1:def 3;
|[1,1]| `2 = 1 by EUCLID:52;
then A9: |[1,1]| in dom f by ;
then A10: f . |[1,1]| in rng f by FUNCT_1:def 3;
reconsider p1 = f . , p2 = f . |[1,1]| as Point of () by A2, A8, A10;
take p1 ; :: thesis: ex p2 being Point of () 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 ; :: thesis: ( p1 in P & p2 in P )
thus ( p1 in P & p2 in P ) by ; :: thesis: verum