let X be Subset of REAL ; :: thesis: X c= Cl X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Cl X )
assume A1: x in X ; :: thesis: x in Cl X
set ClX = { A where A is Subset of REAL : ( X c= A & A is closed ) } ;
A2: [#] REAL in { A where A is Subset of REAL : ( X c= A & A is closed ) } ;

now

let Y be set ; :: thesis: ( Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } implies x in Y )
assume Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } ; :: thesis: x in Y
then consider YY being Subset of REAL such that
A3: ( YY = Y & X c= YY & YY is closed ) ;
thus x in Y by A1, A3; :: thesis: verum

end;

hence x in Cl X by A2, SETFAM_1:def 1; :: thesis: verum