let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; :: thesis: T @--> is strongly-normalizing
set R = T @--> ;
set Q = the InternalRel of T;
A1: field (T @--> ) c= field the InternalRel of T by Th67, RELAT_1:31;
A2: T @--> c= the InternalRel of T by Th67;
T @--> is co-well_founded

proof

let Y be set ; :: according to REWRITE1:def 16 :: thesis: ( not Y c= field (T @--> ) or Y = {} or ex b₁ being set st
( b₁ in Y & ( for b₂ being set holds
( not b₂ in Y or b₁ = b₂ or not [b₁,b₂] in T @--> ) ) ) )
assume that
A3: Y c= field (T @--> ) and
A4: Y <> {} ; :: thesis: ex b₁ being set st
( b₁ in Y & ( for b₂ being set holds
( not b₂ in Y or b₁ = b₂ or not [b₁,b₂] in T @--> ) ) )
Y c= field the InternalRel of T by A1, A3, XBOOLE_1:1;
then consider a being set such that
A5: a in Y and
A6: for b being set st b in Y & a <> b holds
not [a,b] in the InternalRel of T by A4, REWRITE1:def 16;
take a ; :: thesis: ( a in Y & ( for b₁ being set holds
( not b₁ in Y or a = b₁ or not [a,b₁] in T @--> ) ) )
thus ( a in Y & ( for b₁ being set holds
( not b₁ in Y or a = b₁ or not [a,b₁] in T @--> ) ) ) by A2, A5, A6; :: thesis: verum

end;

then T @--> is co-well_founded irreflexive Relation by Th69;
hence T @--> is strongly-normalizing ; :: thesis: verum