let p, q be Point of (TOP-REAL 2); ( p `1 = q `1 iff LSeg (p,q) is vertical )
set P = LSeg (p,q);
thus
( p `1 = q `1 implies LSeg (p,q) is vertical )
( LSeg (p,q) is vertical implies p `1 = q `1 )proof
assume A1:
p `1 = q `1
;
LSeg (p,q) is vertical
let p1 be
Point of
(TOP-REAL 2);
SPPOL_1:def 3 for q being Point of (TOP-REAL 2) st p1 in LSeg (p,q) & q in LSeg (p,q) holds
p1 `1 = q `1 let p2 be
Point of
(TOP-REAL 2);
( p1 in LSeg (p,q) & p2 in LSeg (p,q) implies p1 `1 = p2 `1 )
assume A2:
p1 in LSeg (
p,
q)
;
( not p2 in LSeg (p,q) or p1 `1 = p2 `1 )
assume
p2 in LSeg (
p,
q)
;
p1 `1 = p2 `1
then A3:
(
p `1 <= p2 `1 &
p2 `1 <= p `1 )
by A1, TOPREAL1:3;
(
p `1 <= p1 `1 &
p1 `1 <= p `1 )
by A1, A2, TOPREAL1:3;
then
p `1 = p1 `1
by XXREAL_0:1;
hence
p1 `1 = p2 `1
by A3, XXREAL_0:1;
verum
end;
( p in LSeg (p,q) & q in LSeg (p,q) )
by RLTOPSP1:68;
hence
( LSeg (p,q) is vertical implies p `1 = q `1 )
; verum