:: deftheorem Def30 defines commutative ABCMIZ_0:def 30 :
for T being non empty reflexive transitive non void TAS-structure holds
( T is commutative iff for t1, t2 being type of T
for a being adjective of T st a is_properly_applicable_to t1 & a ast t1 <= t2 holds
ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t1 "\/" t2 & A ast (t1 "\/" t2) = t2 ) );