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

proof

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

proof

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

end;

assume A5: x = q ; :: thesis: x in (LSeg (p,q)) /\ (LSeg (q,r))
then A6: x in LSeg (q,r) by RLTOPSP1:68;
x in LSeg (p,q) by A5, RLTOPSP1:68;
hence x in (LSeg (p,q)) /\ (LSeg (q,r)) by A6, XBOOLE_0:def 4; :: thesis: verum

end;

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