let T be TopSpace; :: thesis: for A being Subset of T holds
( Int (Cl A) is regular_open & Cl (Int A) is regular_closed )
let A be Subset of T; :: thesis: ( Int (Cl A) is regular_open & Cl (Int A) is regular_closed )
A1: Cl (Int (Cl (Int A))) = Cl (Int A) by TOPS_1:26;
Int (Cl (Int (Cl A))) = Int (Cl A) by TDLAT_1:5;
hence ( Int (Cl A) is regular_open & Cl (Int A) is regular_closed ) by A1, TOPS_1:def 7, TOPS_1:def 8; :: thesis: verum