let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; :: thesis: for t1, t2 being type of T st t1 <= t2 holds
radix t1 <= radix t2
set R = T @--> ;
let t1, t2 be type of T; :: thesis: ( t1 <= t2 implies radix t1 <= radix t2 )
assume A1: t1 <= t2 ; :: thesis: radix t1 <= radix t2
t2 <= radix t2 by Th67, Th78;
then A2: t1 <= radix t2 by A1, YELLOW_0:def 2;
set X = the carrier of T;
defpred S₁[ Element of the carrier of T, Element of the carrier of T] means ( $1 <= radix t2 implies $2 <= radix t2 );
A3: for x, y, z being Element of the carrier of T st S₁[x,y] & S₁[y,z] holds
S₁[x,z] ;

A4: now :: thesis: for x, y being Element of the carrier of T st [x,y] in T @--> holds
S₁[x,y]

let x, y be Element of the carrier of T; :: thesis: ( [x,y] in T @--> implies S₁[x,y] )
reconsider t1 = x, t2 = y as type of T ;
assume [x,y] in T @--> ; :: thesis: S₁[x,y]
then ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) by Def31;
hence S₁[x,y] by Th81; :: thesis: verum

end;

A5: for x being Element of the carrier of T holds S₁[x,x] ;
for x, y being Element of T st T @--> reduces x,y holds
S₁[x,y] from ABCMIZ_0:sch 2(A4, A5, A3);
hence radix t1 <= radix t2 by A2, Th78; :: thesis: verum