reconsider C = [:(NetUniv T), the carrier of T:] as Convergence-Class of T by Def18;
take C ; :: thesis: ( not C is empty & C is topological )
thus not C is empty ; :: thesis: C is topological
thus C is topological :: thesis: verum
proof
thus C is (CONSTANTS) by ZFMISC_1:87; :: according to YELLOW_6:def 25 :: thesis: ( C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) )
thus C is (SUBNETS) by ZFMISC_1:87; :: thesis: ( C is (DIVERGENCE) & C is (ITERATED_LIMITS) )
thus C is (DIVERGENCE) by ZFMISC_1:87; :: thesis: C is (ITERATED_LIMITS)
let X be net of T; :: according to YELLOW_6:def 23 :: thesis: for p being Element of T st [X,p] in C holds
for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C
let p be Element of T; :: thesis: ( [X,p] in C implies for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C )
assume [X,p] in C ; :: thesis: for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C
then A1: X in NetUniv T by ZFMISC_1:87;
let J be net_set of the carrier of X,T; :: thesis: ( ( for i being Element of X holds [(J . i),(X . i)] in C ) implies [(Iterated J),p] in C )
assume A2: for i being Element of X holds [(J . i),(X . i)] in C ; :: thesis: [(Iterated J),p] in C
now :: thesis: for i being Element of X holds J . i in NetUniv T
let i be Element of X; :: thesis: J . i in NetUniv T
[(J . i),(X . i)] in C by A2;
hence J . i in NetUniv T by ZFMISC_1:87; :: thesis: verum
end;
then Iterated J in NetUniv T by A1, Th25;
hence [(Iterated J),p] in C by ZFMISC_1:87; :: thesis: verum
end;