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) <> {} by XBOOLE_0:def 7;
then consider x being Point of (TOP-REAL 2) such that
A3: x in (LSeg p,q) /\ (LSeg r,s) by SUBSET_1:10;
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:63
.= r `2 by A2, A4, SPPOL_1:63 ;
:: thesis: verum