let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (p1,p2) & LSeg (p1,p2) is vertical implies LSeg (p,p2) is vertical )
assume A1: p in LSeg (p1,p2) ; :: thesis: ( not LSeg (p1,p2) is vertical or LSeg (p,p2) is vertical )
assume A2: LSeg (p1,p2) is vertical ; :: thesis: LSeg (p,p2) is vertical
then A3: p1 `1 = p2 `1 by SPPOL_1:16;
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then p `1 = p1 `1 by A1, A2;
hence LSeg (p,p2) is vertical by A3, SPPOL_1:16; :: thesis: verum