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) <> {} 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 `1 = x `1 by A1, SPPOL_1:64
.= r `1 by A2, A4, SPPOL_1:64 ;
:: thesis: verum