for T being non empty 1-sorted
for C being Convergence-Class of T holds
( Convergence (ConvergenceSpace C) = C iff C is topological )