let T be TopSpace; :: thesis: for A being Subset of T holds Int (Cl A) is open_condensed
let A be Subset of T; :: thesis: Int (Cl A) is open_condensed
Int (Cl A) = Int (Cl (Int (Cl A))) by Th5;
hence Int (Cl A) is open_condensed by TOPS_1:def 8; :: thesis: verum