let X be TopSpace; :: thesis: for A being Subset of X holds
( ( A is open & A is closed ) iff Cl A = Int A )
let A be Subset of X; :: thesis: ( ( A is open & A is closed ) iff Cl A = Int A )
thus ( A is open & A is closed implies Cl A = Int A ) :: thesis: ( Cl A = Int A implies ( A is open & A is closed ) )

proof

assume ( A is open & A is closed ) ; :: thesis: Cl A = Int A
then ( Int A = A & Cl A = A ) by PRE_TOPC:52, TOPS_1:55;
hence Cl A = Int A ; :: thesis: verum

end;

assume A1: Cl A = Int A ; :: thesis: ( A is open & A is closed )
( Int A c= A & A c= Cl A ) by PRE_TOPC:48, TOPS_1:44;
hence ( A is open & A is closed ) by A1, XBOOLE_0:def 10; :: thesis: verum