let T be non empty TopSpace; :: thesis: for N being net of T st N in NetUniv T holds
for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) )
let N be net of T; :: thesis: ( N in NetUniv T implies for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) ) )
assume N in NetUniv T ; :: thesis: for p being Point of T st not p in Lim N holds
ex Y being subnet of N st
( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) )
then A1: ex M being strict net of T st
( M = N & the carrier of M in the_universe_of the carrier of T ) by Def11;
let p be Point of T; :: thesis: ( not p in Lim N implies ex Y being subnet of N st
( Y in NetUniv T & ( 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
( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) )
then consider V being a_neighborhood of p such that
A2: not N is_eventually_in V by Def15;
N is_often_in the carrier of T \ V by A2, WAYBEL_0:9;
then reconsider Y = N " ( the carrier of T \ V) as subnet of N by Th22;
take Y ; :: thesis: ( Y in NetUniv T & ( for Z being subnet of Y holds not p in Lim Z ) )
the carrier of Y = the mapping of N " ( the carrier of T \ V) by Def10;
then the carrier of Y in the_universe_of the carrier of T by A1, CLASSES1:def 1;
hence Y in NetUniv T by Def11; :: 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 A3: Y is_often_in V by Th18, Th19;
Y is_eventually_in the carrier of T \ V by Th23;
hence contradiction by A3, WAYBEL_0:10; :: thesis: verum