:: deftheorem Def22 defines sub ABCMIZ_0:def 22 :
for T being non empty non void TA-structure
for b₂ being Function of the adjectives of T, the carrier of T holds
( b₂ = sub T iff for a being adjective of T holds b₂ . a = sup ((types a) \/ (types (non- a))) );