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