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