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

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