let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 `2 <= p2 `2 & p in LSeg (p1,p2) implies ( p1 `2 <= p `2 & p `2 <= p2 `2 ) )
assume that
A1: p1 `2 <= p2 `2 and
A2: p in LSeg (p1,p2) ; :: thesis: ( p1 `2 <= p `2 & p `2 <= p2 `2 )
consider lambda being Real such that
A3: p = ((1 - lambda) * p1) + (lambda * p2) and
A4: 0 <= lambda and
A5: lambda <= 1 by A2;
A6: ((1 - lambda) * p1) `2 = |[((1 - lambda) * (p1 `1)),((1 - lambda) * (p1 `2))]| `2 by EUCLID:57
.= (1 - lambda) * (p1 `2) by EUCLID:52 ;
A7: (lambda * p2) `2 = |[(lambda * (p2 `1)),(lambda * (p2 `2))]| `2 by EUCLID:57
.= lambda * (p2 `2) by EUCLID:52 ;
A8: p `2 = |[((((1 - lambda) * p1) `1) + ((lambda * p2) `1)),((((1 - lambda) * p1) `2) + ((lambda * p2) `2))]| `2 by A3, EUCLID:55
.= ((1 - lambda) * (p1 `2)) + (lambda * (p2 `2)) by A6, A7, EUCLID:52 ;
lambda * (p1 `2) <= lambda * (p2 `2) by A1, A4, XREAL_1:64;
then ((1 - lambda) * (p1 `2)) + (lambda * (p1 `2)) <= p `2 by A8, XREAL_1:7;
hence p1 `2 <= p `2 ; :: thesis: p `2 <= p2 `2
0 <= 1 - lambda by A5, XREAL_1:48;
then (1 - lambda) * (p1 `2) <= (1 - lambda) * (p2 `2) by A1, XREAL_1:64;
then p `2 <= ((1 - lambda) * (p2 `2)) + (lambda * (p2 `2)) by A8, XREAL_1:6;
hence p `2 <= p2 `2 ; :: thesis: verum