let GX be TopStruct ; :: thesis: for R being Subset of GX st R is closed_condensed holds
Fr (Int R) = Fr R
let R be Subset of GX; :: thesis: ( R is closed_condensed implies Fr (Int R) = Fr R )
assume R is closed_condensed ; :: thesis: Fr (Int R) = Fr R
then R = Cl (Int R) by Def7;
hence Fr (Int R) = Fr R ; :: thesis: verum