theorem Th86: :: CLASSES5:84

for C being CategorySet holds CatToSet (SetToCat C) = C