:: deftheorem Def20 defines (CONSTANTS) YELLOW_6:def 20 :
for T being non empty 1-sorted
for C being Convergence-Class of T holds
( C is (CONSTANTS) iff for N being constant net of T st N in NetUniv T holds
[N,(the_value_of N)] in C );