:: deftheorem defines topological YELLOW_6:def 25 :
for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is topological iff ( C is (CONSTANTS) & C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) ) );