let p, q be Point of (TOP-REAL 2); :: thesis: ( p <> q & LSeg (p,q) is vertical implies <*p,q*> is being_S-Seq )
assume that
A1: p <> q and
A2: LSeg (p,q) is vertical ; :: thesis: <*p,q*> is being_S-Seq
p `1 = q `1 by A2, SPPOL_1:16;
hence <*p,q*> is being_S-Seq by A1, SPPOL_2:43; :: thesis: verum