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:3
.= (Cl (A `)) ` ;
hence Int A = (Cl (A `)) ` ; :: thesis: verum