let x, X be set ; :: thesis: ( x in subset-closed_closure_of X iff ex y being set st
( x c= y & y in X ) )
set B = { (bool x1) where x1 is Element of X : x1 in X } ;
consider F being subset-closed set such that
A1: F = union { (bool x1) where x1 is Element of X : x1 in X } and
A2: ( X c= F & ( for Y being set st X c= Y & Y is subset-closed holds
F c= Y ) ) by Lm1;
A3: F = subset-closed_closure_of X by A2, Def1;

hereby :: thesis: ( ex y being set st
( x c= y & y in X ) implies x in subset-closed_closure_of X )

assume x in subset-closed_closure_of X ; :: thesis: ex y being set st
( x c= y & y in X )
then consider y being set such that
A4: x in y and
A5: y in { (bool x1) where x1 is Element of X : x1 in X } by A1, A3, TARSKI:def 4;
consider x1 being Element of X such that
A6: ( bool x1 = y & x1 in X ) by A5;
reconsider y = x1 as set ;
take y = y; :: thesis: ( x c= y & y in X )
thus ( x c= y & y in X ) by A4, A6; :: thesis: verum

end;

given y being set such that A7: x c= y and
A8: y in X ; :: thesis: x in subset-closed_closure_of X
bool y in { (bool x1) where x1 is Element of X : x1 in X } by A8;
hence x in subset-closed_closure_of X by A1, A3, A7, TARSKI:def 4; :: thesis: verum