let n be Element of NAT ; :: thesis: for p, p1, p2 being Point of (TOP-REAL n) holds
( not p is_extremal_in LSeg (p1,p2) or p = p1 or p = p2 )
let p, p1, p2 be Point of (TOP-REAL n); :: thesis: ( not p is_extremal_in LSeg (p1,p2) or p = p1 or p = p2 )
assume A1: p is_extremal_in LSeg (p1,p2) ; :: thesis: ( p = p1 or p = p2 )
then p in LSeg (p1,p2) by Def1;
hence ( p = p1 or p = p2 ) by A1, Def1; :: thesis: verum