let T be TopSpace; :: thesis: for A being Subset of T st A is regular_open holds
A ` is regular_closed
let A be Subset of T; :: thesis: ( A is regular_open implies A ` is regular_closed )
assume A is regular_open ; :: thesis: A ` is regular_closed
then Int (Cl A) = A by TOPS_1:def 8;
then Cl ((Cl A) `) = A ` by TDLAT_3:2;
then Cl (Int (A `)) = A ` by TDLAT_3:3;
hence A ` is regular_closed by TOPS_1:def 7; :: thesis: verum