let T be TopSpace; :: thesis: ( [#] T is regular_open & [#] T is regular_closed )

A1: Int ([#] T) = [#] T by TOPS_1:15;

Cl ([#] T) = [#] T by TOPS_1:2;

hence ( [#] T is regular_open & [#] T is regular_closed ) by A1, TOPS_1:def 7, TOPS_1:def 8; :: thesis: verum

A1: Int ([#] T) = [#] T by TOPS_1:15;

Cl ([#] T) = [#] T by TOPS_1:2;

hence ( [#] T is regular_open & [#] T is regular_closed ) by A1, TOPS_1:def 7, TOPS_1:def 8; :: thesis: verum