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