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

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