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