:: deftheorem Def24 defines ConvergenceSpace YELLOW_6:def 24 :
for S being non empty 1-sorted
for C being Convergence-Class of S
for b₃ being strict TopStruct holds
( b₃ = ConvergenceSpace C iff ( the carrier of b₃ = the carrier of S & the topology of b₃ = { V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V } ) );