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

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