let p1, p2, p be Point of (TOP-REAL 2); :: thesis: for a being Real st p in LSeg p1,p2 & p1 `1 <= a & p2 `1 <= a holds
p `1 <= a
let a be Real; :: thesis: ( p in LSeg p1,p2 & p1 `1 <= a & p2 `1 <= a implies p `1 <= a )
assume A1: ( p in LSeg p1,p2 & p1 `1 <= a & p2 `1 <= a ) ; :: thesis: p `1 <= a
then consider r being Real such that
A3: p = ((1 - r) * p1) + (r * p2) and
A2: ( 0 <= r & r <= 1 ) ;
A4: p `1 = (((1 - r) * p1) `1 ) + ((r * p2) `1 ) by A3, TOPREAL3:7
.= (((1 - r) * p1) `1 ) + (r * (p2 `1 )) by TOPREAL3:9
.= ((1 - r) * (p1 `1 )) + (r * (p2 `1 )) by TOPREAL3:9 ;
1 - r >= 0 by A2, XREAL_1:50;
then A5: (1 - r) * (p1 `1 ) <= (1 - r) * a by A1, XREAL_1:66;
A6: r * (p2 `1 ) <= r * a by A1, A2, XREAL_1:66;
((1 - r) * a) + (r * a) = a ;
hence p `1 <= a by A4, A5, A6, XREAL_1:9; :: thesis: verum