:: deftheorem Def13 defines types ABCMIZ_0:def 13 :
for T being non empty TA-structure
for A being Subset of the adjectives of T
for b₃ being Subset of T holds
( b₃ = types A iff for t being type of T holds
( t in b₃ iff for a being adjective of T st a in A holds
t in types a ) );