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 (Cl (Int (Cl A))) c= Int (Cl A) by Th3, TOPS_1:48;
Int (Int (Cl A)) c= Int (Cl (Int (Cl A))) by PRE_TOPC:48, TOPS_1:48;
hence Int (Cl A) = Int (Cl (Int (Cl A))) by A1, XBOOLE_0:def 10; :: thesis: verum