:: deftheorem Def1 defines power-closed CLASSES3:def 1 :
for X being set holds
( X is power-closed iff for Y being set st Y in X holds
bool Y in X );