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