let p, p1, p2, q be Point of (TOP-REAL 2); ( p1 in LSeg (p,q) & p2 in LSeg (p,q) & p1 `1 <> p2 `1 & p1 `2 = p2 `2 implies LSeg (p,q) is horizontal )
assume
p1 in LSeg (p,q)
; ( not p2 in LSeg (p,q) or not p1 `1 <> p2 `1 or not p1 `2 = p2 `2 or LSeg (p,q) is horizontal )
then consider r1 being Real such that
A1:
p1 = ((1 - r1) * p) + (r1 * q)
and
0 <= r1
and
r1 <= 1
;
assume
p2 in LSeg (p,q)
; ( not p1 `1 <> p2 `1 or not p1 `2 = p2 `2 or LSeg (p,q) is horizontal )
then consider r2 being Real such that
A2:
p2 = ((1 - r2) * p) + (r2 * q)
and
0 <= r2
and
r2 <= 1
;
assume that
A3:
p1 `1 <> p2 `1
and
A4:
p1 `2 = p2 `2
; LSeg (p,q) is horizontal
(p `2) - ((r1 * (p `2)) - (r1 * (q `2))) =
((1 - r1) * (p `2)) + (r1 * (q `2))
.=
((1 - r1) * (p `2)) + ((r1 * q) `2)
by TOPREAL3:4
.=
(((1 - r1) * p) `2) + ((r1 * q) `2)
by TOPREAL3:4
.=
p1 `2
by A1, TOPREAL3:2
.=
(((1 - r2) * p) `2) + ((r2 * q) `2)
by A2, A4, TOPREAL3:2
.=
((1 - r2) * (p `2)) + ((r2 * q) `2)
by TOPREAL3:4
.=
((1 * (p `2)) - (r2 * (p `2))) + (r2 * (q `2))
by TOPREAL3:4
.=
(p `2) - ((r2 * (p `2)) - (r2 * (q `2)))
;
then A5:
(r1 - r2) * (p `2) = (r1 - r2) * (q `2)
;
r1 - r2 <> 0
by A1, A2, A3;
then
p `2 = q `2
by A5, XCMPLX_1:5;
hence
LSeg (p,q) is horizontal
by Th15; verum