:: deftheorem defines ~= CLASSES5:def 31 :
for C, D being CategorySet holds
( C ~= D iff SetToCat C ~= SetToCat D );