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:37;
p1 in LSeg p1,p2 by RLTOPSP1:69;
then p `1 = p1 `1 by A1, A2, SPPOL_1:def 3;
hence LSeg p,p2 is vertical by A3, SPPOL_1:37; :: thesis: verum