let T be TopSpace; :: thesis: for A being Subset of T holds
( ( A is open & A is closed ) iff Fr A = {} )
let A be Subset of T; :: thesis: ( ( A is open & A is closed ) iff Fr A = {} )

hereby :: thesis: ( Fr A = {} implies ( A is open & A is closed ) )

assume A1: ( A is open & A is closed ) ; :: thesis: Fr A = {}
then A2: Int A = A by TOPS_1:55;
Fr A = A \ (Int A) by A1, TOPS_1:77
.= {} by A2, XBOOLE_1:37 ;
hence Fr A = {} ; :: thesis: verum

end;

assume A3: Fr A = {} ; :: thesis: ( A is open & A is closed )
A4: A c= Cl A by PRE_TOPC:48;
Fr A = (Cl A) \ (Int A) by Th10;
then A5: Cl A c= Int A by A3, XBOOLE_1:37;
A6: Int A c= A by TOPS_1:44;
then Cl A c= A by A5, XBOOLE_1:1;
then Cl A = A by A4, XBOOLE_0:def 10;
hence ( A is open & A is closed ) by A5, A6, XBOOLE_0:def 10; :: thesis: verum