:: deftheorem defines subjected ABCMIZ_0:def 25 :
for T being non empty non void TAS-structure holds
( T is subjected iff for a being adjective of T holds
( (types a) \/ (types (non- a)) is_<=_than sub a & ( types a <> {} & types (non- a) <> {} implies sub a = sup ((types a) \/ (types (non- a))) ) ) );