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:2
.=
(((1 - r) * p1) `1) + (r * (p2 `1))
by TOPREAL3:4
.=
((1 - r) * (p1 `1)) + (r * (p2 `1))
by TOPREAL3:4
;
1 - r >= 0
by A6, XREAL_1:48;
then A8:
(1 - r) * (p1 `1) <= (1 - r) * a
by A2, XREAL_1:64;
A9:
((1 - r) * a) + (r * a) = a
;
r * (p2 `1) <= r * a
by A3, A5, XREAL_1:64;
hence
p `1 <= a
by A7, A8, A9, XREAL_1:7; verum