theorem Th56: :: CLASSES2:56

for U being Universe holds {} in U