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