theorem :: ABCMIZ_0:79

for T being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for t being type of T holds t <= radix t by Th67, Th78;