let X be set ; :: thesis: subset-closed_closure_of {X} = bool X
set f = subset-closed_closure_of {X};
A1: X in {X} by TARSKI:def 1;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: bool X c= subset-closed_closure_of {X}

let x be object ; :: thesis: ( x in subset-closed_closure_of {X} implies x in bool X )
reconsider xx = x as set by TARSKI:1;
assume x in subset-closed_closure_of {X} ; :: thesis: x in bool X
then consider y being set such that
A2: xx c= y and
A3: y in {X} by Th2;
y = X by A3, TARSKI:def 1;
hence x in bool X by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool X or x in subset-closed_closure_of {X} )
assume x in bool X ; :: thesis: x in subset-closed_closure_of {X}
hence x in subset-closed_closure_of {X} by A1, Th2; :: thesis: verum