let R be non empty transitive antisymmetric RelStr ; :: thesis: for f being sequence of R st f is descending holds
for j, i being Nat st i < j holds
( f . i <> f . j & [(f . j),(f . i)] in the InternalRel of R )

let f be sequence of R; :: thesis: ( f is descending implies for j, i being Nat st i < j holds
( f . i <> f . j & [(f . j),(f . i)] in the InternalRel of R ) )

assume A1: f is descending ; :: thesis: for j, i being Nat st i < j holds
( f . i <> f . j & [(f . j),(f . i)] in the InternalRel of R )

set IR = the InternalRel of R;
set CR = the carrier of R;
A2: the InternalRel of R is_transitive_in the carrier of R by ORDERS_2:def 3;
A3: the InternalRel of R is_antisymmetric_in the carrier of R by ORDERS_2:def 4;
defpred S1[ Nat] means for i being Nat st i < \$1 holds
( f . i <> f . \$1 & [(f . \$1),(f . i)] in the InternalRel of R );
A4: S1[ 0 ] ;
now :: thesis: for j being Nat st ( for i being Nat st i < j holds
( f . i <> f . j & [(f . j),(f . i)] in the InternalRel of R ) ) holds
for i being Nat st i < j + 1 holds
( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R )
let j be Nat; :: thesis: ( ( for i being Nat st i < j holds
( f . i <> f . j & [(f . j),(f . i)] in the InternalRel of R ) ) implies for i being Nat st i < j + 1 holds
( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R ) )

assume A5: for i being Nat st i < j holds
( f . i <> f . j & [(f . j),(f . i)] in the InternalRel of R ) ; :: thesis: for i being Nat st i < j + 1 holds
( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R )

let i be Nat; :: thesis: ( i < j + 1 implies ( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R ) )
assume A6: i < j + 1 ; :: thesis: ( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R )
now :: thesis: ( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R )
per cases ( i > j or i = j or i < j ) by XXREAL_0:1;
suppose i > j ; :: thesis: ( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R )
hence ( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R ) by ; :: thesis: verum
end;
suppose i = j ; :: thesis: ( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R )
hence ( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R ) by A1; :: thesis: verum
end;
suppose i < j ; :: thesis: ( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R )
then A7: [(f . j),(f . i)] in the InternalRel of R by A5;
A8: f . (j + 1) <> f . j by A1;
[(f . (j + 1)),(f . j)] in the InternalRel of R by A1;
hence ( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R ) by A2, A3, A7, A8; :: thesis: verum
end;
end;
end;
hence ( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R ) ; :: thesis: verum
end;
then A9: for j being Nat st S1[j] holds
S1[j + 1] ;
thus for j being Nat holds S1[j] from NAT_1:sch 2(A4, A9); :: thesis: verum