let p, q, r, s be Point of (TOP-REAL 2); :: thesis: ( LSeg (p,q) is vertical & LSeg (r,s) is vertical & LSeg (p,q) meets LSeg (r,s) implies p `1 = r `1 )
assume that
A1: LSeg (p,q) is vertical and
A2: LSeg (r,s) is vertical ; :: thesis: ( not LSeg (p,q) meets LSeg (r,s) or p `1 = r `1 )
assume LSeg (p,q) meets LSeg (r,s) ; :: thesis: p `1 = r `1
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 `1 = x `1 by A1, SPPOL_1:41
.= r `1 by A2, A4, SPPOL_1:41 ;
:: thesis: verum