let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for P, Q being Subset of (TOP-REAL n) st p is_extremal_in P & Q c= P & p in Q holds
p is_extremal_in Q
let p be Point of (TOP-REAL n); :: thesis: for P, Q being Subset of (TOP-REAL n) st p is_extremal_in P & Q c= P & p in Q holds
p is_extremal_in Q
let P, Q be Subset of (TOP-REAL n); :: thesis: ( p is_extremal_in P & Q c= P & p in Q implies p is_extremal_in Q )
assume that
A1: p is_extremal_in P and
A2: Q c= P ; :: thesis: ( not p in Q or p is_extremal_in Q )
assume p in Q ; :: thesis: p is_extremal_in Q
hence p in Q ; :: 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= Q & 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= Q & not p = p1 implies p = p2 )
assume A3: p in LSeg (p1,p2) ; :: thesis: ( not LSeg (p1,p2) c= Q or p = p1 or p = p2 )
assume LSeg (p1,p2) c= Q ; :: thesis: ( p = p1 or p = p2 )
then LSeg (p1,p2) c= P by A2;
hence ( p = p1 or p = p2 ) by A1, A3; :: thesis: verum