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

A2: now :: thesis: for Y being set st Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } holds
x in Y

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 ex YY being Subset of REAL st
( YY = Y & X c= YY & YY is closed ) ;
hence x in Y by A1; :: thesis: verum

end;

X c= [#] REAL by MEMBERED:3;
then [#] REAL in { A where A is Subset of REAL : ( X c= A & A is closed ) } ;
hence x in Cl X by A2, SETFAM_1:def 1; :: thesis: verum