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 set holds
( x in (LSeg p,q) /\ (LSeg q,r) iff x = q )

proof

let x be set ; :: 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 p,q & x in LSeg q,r ) by A3, XBOOLE_0:def 4;
then ( x `1 = q `1 & x `2 = q `2 ) by A1, A2, SPPOL_1:63, SPPOL_1:64;
hence x = q by TOPREAL3:11; :: thesis: verum

end;

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

end;

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