let p1, p, q, p2 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:9
.=
(((1 - r1) * p) `2 ) + ((r1 * q) `2 )
by TOPREAL3:9
.=
p1 `2
by A1, TOPREAL3:7
.=
(((1 - r2) * p) `2 ) + ((r2 * q) `2 )
by A2, A4, TOPREAL3:7
.=
((1 - r2) * (p `2 )) + ((r2 * q) `2 )
by TOPREAL3:9
.=
((1 * (p `2 )) - (r2 * (p `2 ))) + (r2 * (q `2 ))
by TOPREAL3:9
.=
(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 Th36; verum