:: deftheorem defines have_the_same_composition YELLOW20:def 1 :
for A, B being AltCatStr holds
( A,B have_the_same_composition iff for a1, a2, a3 being object holds the Comp of A . [a1,a2,a3] tolerates the Comp of B . [a1,a2,a3] );