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 p1 in LSeg p,q ; :: thesis: ( not p2 in LSeg p,q or p1 `1 = p2 `1 )
then ( p `1 <= p1 `1 & p1 `1 <= p `1 ) by A1, TOPREAL1:9;
then A2: p `1 = p1 `1 by XXREAL_0:1;
assume p2 in LSeg p,q ; :: thesis: p1 `1 = p2 `1
then ( p `1 <= p2 `1 & p2 `1 <= p `1 ) by A1, TOPREAL1:9;
hence p1 `1 = p2 `1 by A2, XXREAL_0:1; :: thesis: verum

end;

( p in LSeg p,q & q in LSeg p,q ) by TOPREAL1:6;
hence ( LSeg p,q is vertical implies p `1 = q `1 ) by Def3; :: thesis: verum