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:18, TOPS_1:19;
hence Int A c= Int (Cl (Int A)) ; :: thesis: verum