let R be non empty RelStr ; :: thesis: for s being sequence of R
for j being Nat st s is descending holds
s ^\ j is descending
let s1 be sequence of R; :: thesis: for j being Nat st s1 is descending holds
s1 ^\ j is descending
let j be Nat; :: thesis: ( s1 is descending implies s1 ^\ j is descending )
assume A1: s1 is descending ; :: thesis: s1 ^\ j is descending
set s2 = s1 ^\ j;
set IR = the InternalRel of R;

now

let n be Nat; :: thesis: ( (s1 ^\ j) . (n + 1) <> (s1 ^\ j) . n & [((s1 ^\ j) . (n + 1)),((s1 ^\ j) . n)] in the InternalRel of R )
set nj = n + j;
A2: (s1 ^\ j) . n = s1 . (n + j) by NAT_1:def 3;
A3: (s1 ^\ j) . (n + 1) = s1 . ((n + 1) + j) by NAT_1:def 3
.= s1 . ((n + j) + 1) ;
hence (s1 ^\ j) . (n + 1) <> (s1 ^\ j) . n by A1, A2, WELLFND1:def 6; :: thesis: [((s1 ^\ j) . (n + 1)),((s1 ^\ j) . n)] in the InternalRel of R
thus [((s1 ^\ j) . (n + 1)),((s1 ^\ j) . n)] in the InternalRel of R by A1, A2, A3, WELLFND1:def 6; :: thesis: verum

end;

hence s1 ^\ j is descending by WELLFND1:def 6; :: thesis: verum