take {} T ; :: thesis: ( {} T is regular_open & {} T is regular_closed )
thus ( {} T is regular_open & {} T is regular_closed ) ; :: thesis: verum