theorem Th10: :: ABCMIZ_0:10

for T being reflexive transitive antisymmetric with_suprema TA-structure st T is adj-structured holds
for t1, t2 being type of T st t1 <= t2 holds
adjs t2 c= adjs t1