let T be SubSpace of TOP-REAL 2; ( the carrier of T is Simple_closed_curve implies T is pathwise_connected )
assume A1:
the carrier of T is Simple_closed_curve
; T is pathwise_connected
then reconsider P = the carrier of T as Simple_closed_curve ;
let a, b be Point of T; BORSUK_2:def 3 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
;
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
;
BORSUK_2:def 1 ( f is continuous & f . 0 = a & f . 1 = b )
f1 is
continuous
by A6;
hence
f is
continuous
by A5, PRE_TOPC:26;
( f . 0 = a & f . 1 = b )thus
(
f . 0 = a &
f . 1
= b )
by A7;
verum end;