theorem Th19: :: ABCMIZ_0:19

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