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