theorem Th77: :: ABCMIZ_0:77

for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure holds
( T @--> is with_Church-Rosser_property & T @--> is with_UN_property )