:: deftheorem Def22 defines (DIVERGENCE) YELLOW_6:def 22 :
for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is (DIVERGENCE) iff for X being net of T
for p being Element of T st X in NetUniv T & not [X,p] in C holds
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) ) );