theorem Th7: :: SIMPLEX0:7

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