for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for t1, t2 being type of T st T @--> reduces t1,t2 holds
t1 <= t2