let X be set ; :: thesis: ( X is subset-closed implies subset-closed_closure_of X = X )
set f = subset-closed_closure_of X;
assume A1: X is subset-closed ; :: thesis: subset-closed_closure_of X = X
thus subset-closed_closure_of X c= X :: according to XBOOLE_0:def 10 :: thesis: X c= subset-closed_closure_of X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in subset-closed_closure_of X or x in X )
assume x in subset-closed_closure_of X ; :: thesis: x in X
then ex y being set st
( x c= y & y in X ) by Th2;
hence x in X by A1, CLASSES1:def 1; :: thesis: verum

end;

thus X c= subset-closed_closure_of X by Def1; :: thesis: verum