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