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:15;
hence <*p,q*> is being_S-Seq by A1, SPPOL_2:43; :: thesis: verum