set A = the non empty transitive strict associative with_units AltCatStr ;
take the non empty transitive strict associative with_units AltCatStr ; :: thesis: ( the non empty transitive strict associative with_units AltCatStr is transitive & the non empty transitive strict associative with_units AltCatStr is associative & the non empty transitive strict associative with_units AltCatStr is with_units & the non empty transitive strict associative with_units AltCatStr is strict )
thus ( the non empty transitive strict associative with_units AltCatStr is transitive & the non empty transitive strict associative with_units AltCatStr is associative & the non empty transitive strict associative with_units AltCatStr is with_units & the non empty transitive strict associative with_units AltCatStr is strict ) ; :: thesis: verum