consider C being category;
take C ; :: thesis: ( C is transitive & C is with_units & C is reflexive )
thus ( C is transitive & C is with_units & C is reflexive ) ; :: thesis: verum