let n be Element of 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, XBOOLE_1:1;
hence ( p = p1 or p = p2 ) by A1, A3, Def1; :: thesis: verum