let p, q, r, s be Point of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: ( not LSeg (p,q) meets LSeg (r,s) or p `2 = r `2 )
assume LSeg (p,q) meets LSeg (r,s) ; :: thesis: 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 ;
:: thesis: verum