for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure holds T @--> is irreflexive