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