for x, X being set holds
( x in subset-closed_closure_of X iff ex y being set st
( x c= y & y in X ) )