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

( 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