theorem Th26: :: ABCMIZ_0:26

for T being reflexive transitive antisymmetric with_suprema adj-structured TA-structure
for A being Subset of the adjectives of T
for t being type of T st A is_applicable_to t holds
(types A) /\ (downarrow t) is Ideal of T