let p, p1, p2 be Point of (); :: 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) )
per cases ( p1 `2 <= p2 `2 or p2 `2 <= p1 `2 ) ;
suppose A3: p1 `2 <= p2 `2 ; :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
now :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
per cases ( p `2 < p1 `2 or p2 `2 < p `2 ) by ;
suppose p `2 < p1 `2 ; :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by ; :: thesis: verum
end;
suppose p2 `2 < p `2 ; :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by ; :: thesis: verum
end;
end;
end;
hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) ; :: thesis: verum
end;
suppose A4: p2 `2 <= p1 `2 ; :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
now :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
per cases ( p `2 < p2 `2 or p1 `2 < p `2 ) by ;
suppose p `2 < p2 `2 ; :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by ; :: thesis: verum
end;
suppose p1 `2 < p `2 ; :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) by ; :: thesis: verum
end;
end;
end;
hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) ; :: thesis: verum
end;
end;