theorem Th87: :: CLASSES5:85

for C being strict Category holds SetToCat (CatToSet C) = C