let p, q, r, s be Point of (); :: 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 object holds
( x in (LSeg (p,q)) /\ (LSeg (s,r)) iff x = r )
proof
let x be object ; :: 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 () ;
x in LSeg (p,q) by ;
then A5: x `2 = p `2 by ;
x in LSeg (s,r) by ;
then A6: x `1 = r `1 by ;
p `2 = r `2 by ;
hence x = r by ; :: thesis: verum
end;
assume A7: x = r ; :: thesis: x in (LSeg (p,q)) /\ (LSeg (s,r))
then x in LSeg (s,r) by RLTOPSP1:68;
hence x in (LSeg (p,q)) /\ (LSeg (s,r)) by ; :: thesis: verum
end;
hence (LSeg (p,q)) /\ (LSeg (s,r)) = {r} by TARSKI:def 1; :: thesis: verum