theorem Th88: :: CLASSES5:86

for U being Universe
for C being Category holds
( C is U -element iff CatToSet C is U -set )