let X be TopSpace; :: thesis: for C being Subset of X holds Cl C = (Int (C `)) `
let C be Subset of X; :: thesis: Cl C = (Int (C `)) `
thus Cl C = ((Cl ((C `) `)) `) `
.= (Int (C `)) ` by TOPS_1:def 1 ; :: thesis: verum