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