theorem Th56: :: KURATO_1:56

for A being with_non-empty_elements set
for B being set st B c= A holds
B is with_non-empty_elements