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