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:23;
Fr A = A \ (Int A) by A1, TOPS_1:43
.= {} by A2, XBOOLE_1:37 ;
hence Fr A = {} ; :: thesis: verum
end;
assume A3: Fr A = {} ; :: thesis: ( A is open & A is closed )
Fr A = (Cl A) \ (Int A) by Th8;
then A4: Cl A c= Int A by A3, XBOOLE_1:37;
A5: Int A c= A by TOPS_1:16;
then ( A c= Cl A & Cl A c= A ) by A4, PRE_TOPC:18;
then Cl A = A ;
hence ( A is open & A is closed ) by A4, A5, XBOOLE_0:def 10; :: thesis: verum