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

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