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

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

let x, y be Element of T; :: thesis: ( [x,y] in T @--> implies S₁[x,y] )
T @--> c= the InternalRel of T by Th66;
hence ( [x,y] in T @--> implies S₁[x,y] ) by ORDERS_2:def 5; :: thesis: verum

end;

A3: for x being Element 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(A2, A3, A1);
hence ( T @--> reduces t1,t2 implies t1 <= t2 ) ; :: thesis: verum