for X being set st X is subset-closed holds
subset-closed_closure_of X = X by Def1;