for Y being set holds
( Y is subset-closed iff for X being set st X in Y holds
bool X c= Y )