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

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