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

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