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 5;
A3: the InternalRel of R is_antisymmetric_in the carrier of R by ORDERS_2:def 6;
defpred S₁[ Nat] means for i being Nat st i < $1 holds
( f . i <> f . $1 & [(f . $1),(f . i)] in the InternalRel of R );
A4: S₁[ 0 ] ;

now

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

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 A6, NAT_1:13; :: 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, WELLFND1:def 7; :: 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, WELLFND1:def 7;
[(f . (j + 1)),(f . j)] in the InternalRel of R by A1, WELLFND1:def 7;
hence ( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R ) by A2, A3, A7, A8, RELAT_2:def 4, RELAT_2:def 8; :: 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 S₁[j] holds
S₁[j + 1] ;
thus for j being Nat holds S₁[j] from NAT_1:sch 2(A4, A9); :: thesis: verum