let T be SubSpace of TOP-REAL 2; :: thesis: ( the carrier of T is Simple_closed_curve implies T is arcwise_connected )
assume A1:
the carrier of T is Simple_closed_curve
; :: thesis: T is arcwise_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 )
;
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;
consider f1 being
Function of
I[01] ,
((TOP-REAL 2) | P1) such that A4:
f1 is
being_homeomorphism
and A5:
(
f1 . 0 = p1 &
f1 . 1
= p2 )
by A2, TOPREAL1:def 2;
the
carrier of
((TOP-REAL 2) | P1) = P1
by PRE_TOPC:29;
then A6:
the
carrier of
((TOP-REAL 2) | P1) c= P
by A3, XBOOLE_1:7;
then reconsider f =
f1 as
Function of
I[01] ,
T by FUNCT_2:9;
take
f
;
:: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )A7:
(TOP-REAL 2) | P1 is
SubSpace of
T
by A6, TSEP_1:4;
f1 is
continuous
by A4, TOPS_2:def 5;
hence
f is
continuous
by A7, PRE_TOPC:56;
:: thesis: ( f . 0 = a & f . 1 = b )thus
(
f . 0 = a &
f . 1
= b )
by A5;
:: thesis: verum end;