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