:: deftheorem Def11 defines adj-structured ABCMIZ_0:def 11 :
for T being reflexive transitive antisymmetric with_suprema TA-structure holds
( T is adj-structured iff for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) );