let T be non empty SubSpace of TOP-REAL n; ( T is convex implies T is pathwise_connected )
assume A1:
[#] T is convex Subset of (TOP-REAL n)
; TOPALG_2:def 1 T is pathwise_connected
let a, b be Point of T; BORSUK_2:def 3 a,b are_connected
A2:
the carrier of T is Subset of (TOP-REAL n)
by TSEP_1:1;
( a in the carrier of T & b in the carrier of T )
;
then reconsider a1 = a, b1 = b as Point of (TOP-REAL n) by A2;
per cases
( a1 <> b1 or a1 = b1 )
;
suppose A3:
a1 <> b1
;
a,b are_connected
[#] ((TOP-REAL n) | (LSeg (a1,b1))) = LSeg (
a1,
b1)
by PRE_TOPC:def 5;
then A4:
the
carrier of
((TOP-REAL n) | (LSeg (a1,b1))) c= the
carrier of
T
by A1, JORDAN1:def 1;
then A5:
(TOP-REAL n) | (LSeg (a1,b1)) is
SubSpace of
T
by TSEP_1:4;
LSeg (
a1,
b1)
is_an_arc_of a1,
b1
by A3, TOPREAL1:9;
then consider h being
Function of
I[01],
((TOP-REAL n) | (LSeg (a1,b1))) such that A6:
h is
being_homeomorphism
and A7:
(
h . 0 = a1 &
h . 1
= b1 )
by TOPREAL1:def 1;
reconsider f =
h 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 )
h is
continuous
by A6, TOPS_2:def 5;
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;