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

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