set C = the category;
take the category ; :: thesis: ( not the category is empty & the category is reflexive )
thus ( not the category is empty & the category is reflexive ) ; :: thesis: verum