theorem Th3: :: SIMPLEX0:3

for X, Y being set st X c= Y & Y is subset-closed holds
subset-closed_closure_of X c= Y