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 that
A1: A is open and
A2: A is closed ; :: thesis: Cl A = Int A
Int A = A by A1, TOPS_1:23;
hence Cl A = Int A by A2, PRE_TOPC:22; :: thesis: verum

end;

A3: Int A c= A by TOPS_1:16;
A4: A c= Cl A by PRE_TOPC:18;
assume Cl A = Int A ; :: thesis: ( A is open & A is closed )
hence ( A is open & A is closed ) by A3, A4, XBOOLE_0:def 10; :: thesis: verum