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