:: deftheorem defines is_extremal_in SPPOL_1:def 1 :
for n being Nat
for p being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) holds
( p is_extremal_in P iff ( p in P & ( 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 ) ) );