let p, q be Point of (TOP-REAL 2); :: thesis: ( 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 ) :: thesis: ( LSeg (p,q) is vertical implies p `1 = q `1 )

proof

assume A1: p `1 = q `1 ; :: thesis: LSeg (p,q) is vertical
let p1 be Point of (TOP-REAL 2); :: according to SPPOL_1:def 3 :: thesis: 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); :: thesis: ( p1 in LSeg (p,q) & p2 in LSeg (p,q) implies p1 `1 = p2 `1 )
assume A2: p1 in LSeg (p,q) ; :: thesis: ( not p2 in LSeg (p,q) or p1 `1 = p2 `1 )
assume p2 in LSeg (p,q) ; :: thesis: 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; :: thesis: 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 ) ; :: thesis: verum