let T be TopSpace; :: thesis: for A being Subset of T holds Int (Cl A) = Int (Cl (Int (Cl A)))
let A be Subset of T; :: thesis: Int (Cl A) = Int (Cl (Int (Cl A)))
A1: Int (Int (Cl A)) c= Int (Cl (Int (Cl A))) by PRE_TOPC:18, TOPS_1:19;
Int (Cl (Int (Cl A))) c= Int (Cl A) by Th3, TOPS_1:19;
hence Int (Cl A) = Int (Cl (Int (Cl A))) by A1; :: thesis: verum