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