take the_empty_category ; :: thesis: ( the_empty_category is empty & the_empty_category is strict )
thus ( the_empty_category is empty & the_empty_category is strict ) ; :: thesis: verum