let TS be TopSpace; :: thesis: for K being Subset of TS holds Cl (Fr K) = Fr K
let K be Subset of TS; :: thesis: Cl (Fr K) = Fr K
A1: Cl (Cl K) = Cl K ;
Cl (Cl (K ` )) = Cl (K ` ) ;
hence Cl (Fr K) = Fr K by A1, Th34; :: thesis: verum