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 S_{1}[ 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_{1}[ 0 ]
;

_{1}[j] holds

S_{1}[j + 1]
;

thus for j being Nat holds S_{1}[j]
from NAT_1:sch 2(A4, A9); :: thesis: verum

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 S

( f . i <> f . $1 & [(f . $1),(f . i)] in the InternalRel of R );

A4: S

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 )

then A9:
for j being Nat st S( 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 )

end;( 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 )end;

hence
( f . i <> f . (j + 1) & [(f . (j + 1)),(f . i)] in the InternalRel of R )
; :: thesis: verumper cases
( i > j or i = j or i < j )
by XXREAL_0:1;

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 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; :: 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;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

S

thus for j being Nat holds S