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 Th66, RELAT_1:16;
A2: T @--> c= the InternalRel of T by Th66;
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 object st
( b₁ in Y & ( for b₂ being object 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 object st
( b₁ in Y & ( for b₂ being object holds
( not b₂ in Y or b₁ = b₂ or not [b₁,b₂] in T @--> ) ) )
Y c= field the InternalRel of T by A1, A3;
then consider a being object such that
A5: a in Y and
A6: for b being object 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 object holds
( not b₁ in Y or a = b₁ or not [a,b₁] in T @--> ) ) )
thus ( a in Y & ( for b₁ being object 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 Th68;
hence T @--> is strongly-normalizing ; :: thesis: verum