let TS be TopSpace; :: thesis: for K being Subset of TS holds Fr (Fr (Fr K)) = Fr (Fr K)
let K be Subset of TS; :: thesis: Fr (Fr (Fr K)) = Fr (Fr K)
A1: Int (Fr (Fr K)) = {} by Lm4;
Fr (Fr (Fr K)) = (Cl (Fr (Fr K))) \ (Int (Fr (Fr K))) by Lm2
.= Fr (Fr K) by A1, Lm3 ;
hence Fr (Fr (Fr K)) = Fr (Fr K) ; :: thesis: verum