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