let p, q, s 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:49;
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 Th24;
then A9:
((1 - r) * p) `1 = (1 - r) * (p `1)
by EUCLID:52;
r * q = |[(r * (q `1)),(r * (q `2))]|
by Th24;
then A10:
(r * q) `1 = r * (q `1)
by EUCLID:52;
s = |[((((1 - r) * p) `1) + ((r * q) `1)),((((1 - r) * p) `2) + ((r * q) `2))]|
by A6, EUCLID:55;
then A11:
s `1 = ((1 - r) * (p `1)) + (r * (q `1))
by A9, A10, EUCLID:52;
then A12:
(p `1) - (s `1) = r * ((p `1) - (q `1))
;
r < 1
by A3, A6, A8, Th26;
then A13:
1 - r > 0
by XREAL_1:50;
A14:
(q `1) - (p `1) > 0
by A4, XREAL_1:50;
r > 0
by A2, A6, A7, Th25;
then A15:
(p `1) - (s `1) < 0
by A12, A5, XREAL_1:132;
(q `1) - (s `1) = (1 - r) * ((q `1) - (p `1))
by A11;
then
(q `1) - (s `1) > 0
by A14, A13, XREAL_1:129;
hence
( p `1 < s `1 & s `1 < q `1 )
by A15, XREAL_1:47, XREAL_1:48; verum