let TS be TopSpace; :: thesis: for P being Subset of TS holds
( P is open iff Fr P = (Cl P) \ P )
let P be Subset of TS; :: thesis: ( P is open iff Fr P = (Cl P) \ P )

hereby :: thesis: ( Fr P = (Cl P) \ P implies P is open )

assume P is open ; :: thesis: Fr P = (Cl P) \ P
then P = Int P by Th55;
hence Fr P = (Cl P) \ P by Lm4; :: thesis: verum

end;

assume A1: Fr P = (Cl P) \ P ; :: thesis: P is open
A2: Fr P misses (Fr P) ` by XBOOLE_1:79;
A3: ( Fr P c= Cl P & P c= Cl P ) by PRE_TOPC:48, XBOOLE_1:17;
(Cl P) \ (Fr P) = (P \/ (Fr P)) \ (Fr P) by Th65
.= ((Fr P) ` ) /\ (P \/ (Fr P)) by SUBSET_1:32
.= (P /\ ((Fr P) ` )) \/ (((Fr P) ` ) /\ (Fr P)) by XBOOLE_1:23
.= (P \ (Fr P)) \/ ((Fr P) /\ ((Fr P) ` )) by SUBSET_1:32
.= (Int P) \/ ((Fr P) /\ ((Fr P) ` )) by Th74
.= (Int P) \/ ({} TS) by A2, XBOOLE_0:def 7
.= Int P ;
then ( P c= Int P & Int P c= P ) by A1, A3, Lm7, Th44;
hence P is open by XBOOLE_0:def 10; :: thesis: verum