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 object holds

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

hence
(LSeg (p,q)) /\ (LSeg (s,r)) = {r}
by TARSKI:def 1; :: thesis: verum
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)) )

then x in LSeg (s,r) by RLTOPSP1:68;

hence x in (LSeg (p,q)) /\ (LSeg (s,r)) by A3, A7, XBOOLE_0:def 4; :: thesis: verum

end;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 A7:
x = r
; :: thesis: x in (LSeg (p,q)) /\ (LSeg (s,r))
assume A4:
x in (LSeg (p,q)) /\ (LSeg (s,r))
; :: thesis: x = r

then reconsider x = x as Point of (TOP-REAL 2) ;

x in LSeg (p,q) by A4, XBOOLE_0:def 4;

then A5: x `2 = p `2 by A1, SPPOL_1:40;

x in LSeg (s,r) by A4, XBOOLE_0:def 4;

then A6: x `1 = r `1 by A2, SPPOL_1:41;

p `2 = r `2 by A1, A3, SPPOL_1:40;

hence x = r by A5, A6, TOPREAL3:6; :: thesis: verum

end;then reconsider x = x as Point of (TOP-REAL 2) ;

x in LSeg (p,q) by A4, XBOOLE_0:def 4;

then A5: x `2 = p `2 by A1, SPPOL_1:40;

x in LSeg (s,r) by A4, XBOOLE_0:def 4;

then A6: x `1 = r `1 by A2, SPPOL_1:41;

p `2 = r `2 by A1, A3, SPPOL_1:40;

hence x = r by A5, A6, TOPREAL3:6; :: thesis: verum

then x in LSeg (s,r) by RLTOPSP1:68;

hence x in (LSeg (p,q)) /\ (LSeg (s,r)) by A3, A7, XBOOLE_0:def 4; :: thesis: verum