theorem Th89: :: CLASSES5:87

for U being Universe
for C being CategorySet holds
( C is U -set iff SetToCat C is U -element )