let T be non empty TopSpace; :: thesis: for N being net of T
for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
for Z being subnet of Y holds not p in Lim Z
let N be net of T; :: thesis: for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
for Z being subnet of Y holds not p in Lim Z
let p be Point of T; :: thesis: ( not p in Lim N implies ex Y being subnet of N st
for Z being subnet of Y holds not p in Lim Z )
assume not p in Lim N ; :: thesis: ex Y being subnet of N st
for Z being subnet of Y holds not p in Lim Z
then consider V being a_neighborhood of p such that
A1: not N is_eventually_in V by Def15;
N is_often_in the carrier of T \ V by A1, WAYBEL_0:9;
then reconsider Y = N " ( the carrier of T \ V) as subnet of N by Th22;
take Y ; :: thesis: for Z being subnet of Y holds not p in Lim Z
let Z be subnet of Y; :: thesis: not p in Lim Z
assume p in Lim Z ; :: thesis: contradiction
then Z is_eventually_in V by Def15;
then A2: Y is_often_in V by Th18, Th19;
Y is_eventually_in the carrier of T \ V by Th23;
hence contradiction by A2, WAYBEL_0:10; :: thesis: verum