let p, q, r, s be Point of (TOP-REAL 2); :: thesis: ( LSeg p,q is horizontal & LSeg s,r is vertical & r in LSeg p,q implies (LSeg p,q) /\ (LSeg s,r) = {r} )
assume that
A1: LSeg p,q is horizontal and
A2: LSeg s,r is vertical and
A3: r in LSeg p,q ; :: thesis: (LSeg p,q) /\ (LSeg s,r) = {r}
for x being set holds
( x in (LSeg p,q) /\ (LSeg s,r) iff x = r )

proof

let x be set ; :: thesis: ( x in (LSeg p,q) /\ (LSeg s,r) iff x = r )
thus ( x in (LSeg p,q) /\ (LSeg s,r) implies x = r ) :: thesis: ( x = r implies x in (LSeg p,q) /\ (LSeg s,r) )

proof

assume A4: x in (LSeg p,q) /\ (LSeg s,r) ; :: thesis: x = r
then reconsider x = x as Point of (TOP-REAL 2) ;
A5: p `2 = r `2 by A1, A3, SPPOL_1:63;
( x in LSeg p,q & x in LSeg s,r ) by A4, XBOOLE_0:def 4;
then ( x `2 = p `2 & x `1 = r `1 ) by A1, A2, SPPOL_1:63, SPPOL_1:64;
hence x = r by A5, TOPREAL3:11; :: thesis: verum

end;

assume x = r ; :: thesis: x in (LSeg p,q) /\ (LSeg s,r)
then ( x in LSeg p,q & x in LSeg s,r ) by A3, RLTOPSP1:69;
hence x in (LSeg p,q) /\ (LSeg s,r) by XBOOLE_0:def 4; :: thesis: verum

end;

hence (LSeg p,q) /\ (LSeg s,r) = {r} by TARSKI:def 1; :: thesis: verum