consider A being non empty transitive strict associative with_units AltCatStr ;
take A ; :: thesis: ( A is transitive & A is associative & A is with_units & A is strict )
thus ( A is transitive & A is associative & A is with_units & A is strict ) ; :: thesis: verum