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