let n be Nat; :: thesis: for p being Point of (TOP-REAL n) holds p is_extremal_in {p}
let p be Point of (TOP-REAL n); :: thesis: p is_extremal_in {p}
thus p in {p} by TARSKI:def 1; :: according to SPPOL_1:def 1 :: thesis: for p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & LSeg (p1,p2) c= {p} & not p = p1 holds
p = p2
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( p in LSeg (p1,p2) & LSeg (p1,p2) c= {p} & not p = p1 implies p = p2 )
assume that
p in LSeg (p1,p2) and
A1: LSeg (p1,p2) c= {p} ; :: thesis: ( p = p1 or p = p2 )
p2 in LSeg (p1,p2) by RLTOPSP1:68;
hence ( p = p1 or p = p2 ) by A1, TARSKI:def 1; :: thesis: verum