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