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 `) = (Int ((C `) `)) ` by Th1
.= (Int C) ` ; :: thesis: verum