let p1, p2, p be Point of (TOP-REAL 2); :: thesis: ( p1 `1 <= p2 `1 & p in LSeg p1,p2 implies ( p1 `1 <= p `1 & p `1 <= p2 `1 ) )
assume that
A1: p1 `1 <= p2 `1 and
A2: p in LSeg p1,p2 ; :: thesis: ( p1 `1 <= p `1 & p `1 <= p2 `1 )
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) `1 = |[((1 - lambda) * (p1 `1 )),((1 - lambda) * (p1 `2 ))]| `1 by EUCLID:61
.= (1 - lambda) * (p1 `1 ) by EUCLID:56 ;
A7: (lambda * p2) `1 = |[(lambda * (p2 `1 )),(lambda * (p2 `2 ))]| `1 by EUCLID:61
.= lambda * (p2 `1 ) by EUCLID:56 ;
A8: p `1 = |[((((1 - lambda) * p1) `1 ) + ((lambda * p2) `1 )),((((1 - lambda) * p1) `2 ) + ((lambda * p2) `2 ))]| `1 by A3, EUCLID:59
.= ((1 - lambda) * (p1 `1 )) + (lambda * (p2 `1 )) by A6, A7, EUCLID:56 ;
lambda * (p1 `1 ) <= lambda * (p2 `1 ) by A1, A4, XREAL_1:66;
then ((1 - lambda) * (p1 `1 )) + (lambda * (p1 `1 )) <= p `1 by A8, XREAL_1:9;
hence p1 `1 <= p `1 ; :: thesis: p `1 <= p2 `1
0 <= 1 - lambda by A5, XREAL_1:50;
then (1 - lambda) * (p1 `1 ) <= (1 - lambda) * (p2 `1 ) by A1, XREAL_1:66;
then p `1 <= ((1 - lambda) * (p2 `1 )) + (lambda * (p2 `1 )) by A8, XREAL_1:8;
hence p `1 <= p2 `1 ; :: thesis: verum