:: deftheorem Def12 defines types ABCMIZ_0:def 12 :
for T being TA-structure
for a being Element of the adjectives of T
for b₃ being Subset of T holds
( b₃ = types a iff for x being object holds
( x in b₃ iff ex t being type of T st
( x = t & a in adjs t ) ) );