let P be Subset of (TOP-REAL 2); for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds
LE q1,q3,P,p1,p2
let p1, p2, q1, q2, q3 be Point of (TOP-REAL 2); ( LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 implies LE q1,q3,P,p1,p2 )
assume that
A1:
LE q1,q2,P,p1,p2
and
A2:
LE q2,q3,P,p1,p2
; LE q1,q3,P,p1,p2
A3:
q2 in P
by A1;
A4:
now for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 holds
s1 <= s2A5:
[.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) }
by RCOMP_1:def 1;
let g be
Function of
I[01],
((TOP-REAL 2) | P);
for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 holds
s1 <= s2let s1,
s2 be
Real;
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )assume that A6:
g is
being_homeomorphism
and A7:
(
g . 0 = p1 &
g . 1
= p2 &
g . s1 = q1 )
and
0 <= s1
and A8:
(
s1 <= 1 &
g . s2 = q3 &
0 <= s2 &
s2 <= 1 )
;
s1 <= s2 rng g =
[#] ((TOP-REAL 2) | P)
by A6, TOPS_2:def 5
.=
P
by PRE_TOPC:def 5
;
then consider x being
object such that A9:
x in dom g
and A10:
q2 = g . x
by A3, FUNCT_1:def 3;
dom g =
[#] I[01]
by A6, TOPS_2:def 5
.=
the
carrier of
I[01]
;
then consider s3 being
Real such that A11:
(
s3 = x &
0 <= s3 &
s3 <= 1 )
by A9, A5, BORSUK_1:40;
(
s1 <= s3 &
s3 <= s2 )
by A1, A2, A6, A7, A8, A10, A11;
hence
s1 <= s2
by XXREAL_0:2;
verum end;
( q1 in P & q3 in P )
by A1, A2;
hence
LE q1,q3,P,p1,p2
by A4; verum