let p, p1, p2 be Point of (TOP-REAL 2); :: thesis:
assume that
A1: not p in LSeg (p1,p2) and
A2: ( p1 `1 = p2 `1 & p2 `1 = p `1 ) ; :: thesis:

per cases ;

suppose A3: p1 `2 <= p2 `2 ; :: thesis:

now :: thesis:

per cases by A1, A2, GOBOARD7:7;

suppose p `2 < p1 `2 ; :: thesis:

hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A3, GOBOARD7:7; :: thesis:

end;

suppose p2 `2 < p `2 ; :: thesis:

hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A3, GOBOARD7:7; :: thesis:

end;

end;

end;

hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) ; :: thesis:

end;

suppose A4: p2 `2 <= p1 `2 ; :: thesis:

now :: thesis:

per cases by A1, A2, GOBOARD7:7;

suppose p `2 < p2 `2 ; :: thesis:

hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A4, GOBOARD7:7; :: thesis:

end;

suppose p1 `2 < p `2 ; :: thesis:

hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by A2, A4, GOBOARD7:7; :: thesis:

end;

end;

end;

hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) ; :: thesis:

end;

end;