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:
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 in P & b in P ) ;
then reconsider p1 = a, p2 = b as Point of () ;
per cases ( p1 <> p2 or p1 = p2 ) ;
suppose p1 <> p2 ; :: thesis:
then consider P1, P2 being non empty Subset of () 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 (() | P1) = P1 by PRE_TOPC:8;
then A4: the carrier of (() | P1) c= P by ;
then A5: (TOP-REAL 2) | P1 is SubSpace of T by TSEP_1:4;
consider f1 being Function of I,(() | P1) such that
A6: f1 is being_homeomorphism and
A7: ( f1 . 0 = p1 & f1 . 1 = p2 ) by ;
reconsider f = f1 as Function of I,T by ;
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 ; :: thesis: ( f . 0 = a & f . 1 = b )
thus ( f . 0 = a & f . 1 = b ) by A7; :: thesis: verum
end;
suppose A8: p1 = p2 ; :: thesis:
reconsider T1 = T as non empty SubSpace of TOP-REAL 2 by A1;
reconsider a1 = a as Point of T1 ;
reconsider f = I --> a1 as Function of I,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;
end;