let T be SubSpace of TOP-REAL 2; :: thesis: ( the carrier of T is Simple_closed_curve implies T is pathwise_connected )

assume A1: the carrier of T is Simple_closed_curve ; :: thesis: T is pathwise_connected

then reconsider P = the carrier of T as Simple_closed_curve ;

let a, b be Point of T; :: according to BORSUK_2:def 3 :: thesis: a,b are_connected

( a in P & b in P ) ;

then reconsider p1 = a, p2 = b as Point of (TOP-REAL 2) ;

assume A1: the carrier of T is Simple_closed_curve ; :: thesis: T is pathwise_connected

then reconsider P = the carrier of T as Simple_closed_curve ;

let a, b be Point of T; :: according to BORSUK_2:def 3 :: thesis: a,b are_connected

( a in P & b in P ) ;

then reconsider p1 = a, p2 = b as Point of (TOP-REAL 2) ;

per cases
( p1 <> p2 or p1 = p2 )
;

end;

suppose
p1 <> p2
; :: thesis: a,b are_connected

then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that

A2: P1 is_an_arc_of p1,p2 and

P2 is_an_arc_of p1,p2 and

A3: P = P1 \/ P2 and

P1 /\ P2 = {p1,p2} by TOPREAL2:5;

the carrier of ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:8;

then A4: the carrier of ((TOP-REAL 2) | P1) c= P by A3, XBOOLE_1:7;

then A5: (TOP-REAL 2) | P1 is SubSpace of T by TSEP_1:4;

consider f1 being Function of I[01],((TOP-REAL 2) | P1) such that

A6: f1 is being_homeomorphism and

A7: ( f1 . 0 = p1 & f1 . 1 = p2 ) by A2, TOPREAL1:def 1;

reconsider f = f1 as Function of I[01],T by A4, FUNCT_2:7;

take f ; :: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )

f1 is continuous by A6;

hence f is continuous by A5, PRE_TOPC:26; :: thesis: ( f . 0 = a & f . 1 = b )

thus ( f . 0 = a & f . 1 = b ) by A7; :: thesis: verum

end;A2: P1 is_an_arc_of p1,p2 and

P2 is_an_arc_of p1,p2 and

A3: P = P1 \/ P2 and

P1 /\ P2 = {p1,p2} by TOPREAL2:5;

the carrier of ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:8;

then A4: the carrier of ((TOP-REAL 2) | P1) c= P by A3, XBOOLE_1:7;

then A5: (TOP-REAL 2) | P1 is SubSpace of T by TSEP_1:4;

consider f1 being Function of I[01],((TOP-REAL 2) | P1) such that

A6: f1 is being_homeomorphism and

A7: ( f1 . 0 = p1 & f1 . 1 = p2 ) by A2, TOPREAL1:def 1;

reconsider f = f1 as Function of I[01],T by A4, FUNCT_2:7;

take f ; :: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )

f1 is continuous by A6;

hence f is continuous by A5, PRE_TOPC:26; :: thesis: ( f . 0 = a & f . 1 = b )

thus ( f . 0 = a & f . 1 = b ) by A7; :: thesis: verum

suppose A8:
p1 = p2
; :: thesis: a,b are_connected

reconsider T1 = T as non empty SubSpace of TOP-REAL 2 by A1;

reconsider a1 = a as Point of T1 ;

reconsider f = I[01] --> a1 as Function of I[01],T ;

take f ; :: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )

thus f is continuous ; :: thesis: ( f . 0 = a & f . 1 = b )

thus f . 0 = f . j0

.= a ; :: thesis: f . 1 = b

thus f . 1 = f . j1

.= b by A8 ; :: thesis: verum

end;reconsider a1 = a as Point of T1 ;

reconsider f = I[01] --> a1 as Function of I[01],T ;

take f ; :: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )

thus f is continuous ; :: thesis: ( f . 0 = a & f . 1 = b )

thus f . 0 = f . j0

.= a ; :: thesis: f . 1 = b

thus f . 1 = f . j1

.= b by A8 ; :: thesis: verum