theorem :: ABCMIZ_0:25

for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for a, b being adjective of T st a is_applicable_to t & b is_applicable_to a ast t holds
( b is_applicable_to t & a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) )