let p, q, r, s be Point of (TOP-REAL 2); ( LSeg (p,q) is horizontal & LSeg (r,s) is horizontal & LSeg (p,q) meets LSeg (r,s) implies p `2 = r `2 )
assume that
A1:
LSeg (p,q) is horizontal
and
A2:
LSeg (r,s) is horizontal
; ( not LSeg (p,q) meets LSeg (r,s) or p `2 = r `2 )
assume
LSeg (p,q) meets LSeg (r,s)
; p `2 = r `2
then
(LSeg (p,q)) /\ (LSeg (r,s)) <> {}
;
then consider x being Point of (TOP-REAL 2) such that
A3:
x in (LSeg (p,q)) /\ (LSeg (r,s))
by SUBSET_1:4;
A4:
x in LSeg (r,s)
by A3, XBOOLE_0:def 4;
x in LSeg (p,q)
by A3, XBOOLE_0:def 4;
hence p `2 =
x `2
by A1, SPPOL_1:40
.=
r `2
by A2, A4, SPPOL_1:40
;
verum