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