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