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

assume that

A1: not p in LSeg (p1,p2) and

A2: ( p1 `1 = p2 `1 & p2 `1 = p `1 ) ; :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )

assume that

A1: not p in LSeg (p1,p2) and

A2: ( p1 `1 = p2 `1 & p2 `1 = p `1 ) ; :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )

per cases
( p1 `2 <= p2 `2 or p2 `2 <= p1 `2 )
;

end;

suppose A3:
p1 `2 <= p2 `2
; :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )

end;

now :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )

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

suppose A4:
p2 `2 <= p1 `2
; :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )

end;

now :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )

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