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

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