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