let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; :: thesis: for t being type of T holds T @--> reduces t, radix t
let t be type of T; :: thesis: T @--> reduces t, radix t
set R = T @--> ;
T @--> is strongly-normalizing with_UN_property with_Church-Rosser_property Relation by Th69, Th77;
then nf (t,(T @-->)) is_a_normal_form_of t,T @--> by REWRITE1:54;
hence T @--> reduces t, radix t ; :: thesis: verum