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

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