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 )
A1: Fr P misses (Fr P) ` by XBOOLE_1:79;
A2: Int P c= P by Th16;

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 Th23;
hence Fr P = (Cl P) \ P by Lm2; :: thesis: verum

end;

assume A3: Fr P = (Cl P) \ P ; :: thesis: P is open
(Cl P) \ (Fr P) = (P \/ (Fr P)) \ (Fr P) by Th31
.= ((Fr P) `) /\ (P \/ (Fr P)) by SUBSET_1:13
.= (P /\ ((Fr P) `)) \/ (((Fr P) `) /\ (Fr P)) by XBOOLE_1:23
.= (P \ (Fr P)) \/ ((Fr P) /\ ((Fr P) `)) by SUBSET_1:13
.= (Int P) \/ ((Fr P) /\ ((Fr P) `)) by Th40
.= (Int P) \/ ({} TS) by A1
.= Int P ;
then P c= Int P by A3, Lm5, PRE_TOPC:18;
hence P is open by A2, XBOOLE_0:def 10; :: thesis: verum