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