let T be TopSpace; :: thesis: for A being Subset of T holds Int A = (Cl (A ` )) `
let A be Subset of T; :: thesis: Int A = (Cl (A ` )) `
Int A = (Cl (((A ` ) ` ) ` )) ` by TDLAT_3:4
.= (Cl (A ` )) ` ;
hence Int A = (Cl (A ` )) ` ; :: thesis: verum