let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: ( not p in LSeg (p1,p2) & p1 `2 = p2 `2 & p2 `2 = p `2 & not p1 in LSeg (p,p2) implies p2 in LSeg (p,p1) )
assume that
A1: not p in LSeg (p1,p2) and
A2: ( p1 `2 = p2 `2 & p2 `2 = p `2 ) ; :: thesis: ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) )
per cases ( p1 `1 <= p2 `1 or p2 `1 <= p1 `1 ) ;
suppose A3: p1 `1 <= p2 `1 ; :: 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 `1 < p1 `1 or p2 `1 < p `1 ) by A1, A2, GOBOARD7:8;
suppose p `1 < p1 `1 ; :: 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 A2, A3, GOBOARD7:8; :: thesis: verum
end;
suppose p2 `1 < p `1 ; :: 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 A2, A3, GOBOARD7:8; :: thesis: verum
end;
end;
end;
hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) ; :: thesis: verum
end;
suppose A4: p2 `1 <= p1 `1 ; :: 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 `1 < p2 `1 or p1 `1 < p `1 ) by A1, A2, GOBOARD7:8;
suppose p `1 < p2 `1 ; :: 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 A2, A4, GOBOARD7:8; :: thesis: verum
end;
suppose p1 `1 < p `1 ; :: 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 A2, A4, GOBOARD7:8; :: thesis: verum
end;
end;
end;
hence ( p1 in LSeg (p,p2) or p2 in LSeg (p,p1) ) ; :: thesis: verum
end;
end;