reconsider C = [:(NetUniv T), the carrier of T:] as Convergence-Class of T by Def18;
take
C
; ( not C is empty & C is topological )
thus
not C is empty
; C is topological
thus
C is topological
verumproof
thus
C is
(CONSTANTS)
by ZFMISC_1:87;
YELLOW_6:def 25 ( C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) )
thus
C is
(SUBNETS)
by ZFMISC_1:87;
( C is (DIVERGENCE) & C is (ITERATED_LIMITS) )
thus
C is
(DIVERGENCE)
by ZFMISC_1:87;
C is (ITERATED_LIMITS)
let X be
net of
T;
YELLOW_6:def 23 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 Clet p be
Element of
T;
( [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
;
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;
( ( 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
;
[(Iterated J),p] in C
then
Iterated J in NetUniv T
by A1, Th25;
hence
[(Iterated J),p] in C
by ZFMISC_1:87;
verum
end;