let s, p, q be Point of (TOP-REAL 2); ( s in LSeg p,q & s <> p & s <> q & p `1 < q `1 implies ( p `1 < s `1 & s `1 < q `1 ) )
assume that
A1:
s in LSeg p,q
and
A2:
s <> p
and
A3:
s <> q
and
A4:
p `1 < q `1
; ( p `1 < s `1 & s `1 < q `1 )
A5:
(p `1 ) - (q `1 ) < 0
by A4, XREAL_1:51;
consider r being Real such that
A6:
s = ((1 - r) * p) + (r * q)
and
A7:
0 <= r
and
A8:
r <= 1
by A1;
(1 - r) * p = |[((1 - r) * (p `1 )),((1 - r) * (p `2 ))]|
by Th34;
then A9:
((1 - r) * p) `1 = (1 - r) * (p `1 )
by EUCLID:56;
r * q = |[(r * (q `1 )),(r * (q `2 ))]|
by Th34;
then A10:
(r * q) `1 = r * (q `1 )
by EUCLID:56;
s = |[((((1 - r) * p) `1 ) + ((r * q) `1 )),((((1 - r) * p) `2 ) + ((r * q) `2 ))]|
by A6, EUCLID:59;
then A11:
s `1 = ((1 - r) * (p `1 )) + (r * (q `1 ))
by A9, A10, EUCLID:56;
then A12:
(p `1 ) - (s `1 ) = r * ((p `1 ) - (q `1 ))
;
r < 1
by A3, A6, A8, Th36;
then A13:
1 - r > 0
by XREAL_1:52;
A14:
(q `1 ) - (p `1 ) > 0
by A4, XREAL_1:52;
r > 0
by A2, A6, A7, Th35;
then A15:
(p `1 ) - (s `1 ) < 0
by A12, A5, XREAL_1:134;
(q `1 ) - (s `1 ) = (1 - r) * ((q `1 ) - (p `1 ))
by A11;
then
(q `1 ) - (s `1 ) > 0
by A14, A13, XREAL_1:131;
hence
( p `1 < s `1 & s `1 < q `1 )
by A15, XREAL_1:49, XREAL_1:50; verum