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