let I be set ; :: thesis:
let R be asymmetric transitive Relation of I; :: thesis:
let r be RedSequence of R; :: thesis:
let a be object ; :: according to FUNCT_1:def 4 :: thesis:
let b be object ; :: thesis:
assume Z0: ( a in dom r & b in dom r ) ; :: thesis:
then reconsider i = a, j = b as Nat ;
assume Z1: ( r . a = r . b & a <> b ) ; :: thesis:
A1: for i, j being Nat st i > j & i in dom r & j in dom r holds
r . i <> r . j

let i, j be Nat; :: thesis:
assume i > j ; :: thesis:
then A1: i >= j + 1 by NAT_1:13;
assume Z3: i in dom r ; :: thesis:
assume Z4: j in dom r ; :: thesis:
defpred S₁[ Nat] means ( $1 in dom r implies ( [(r . j),(r . $1)] in R & r . $1 <> r . j ) );
A2: S₁[j + 1]

assume j + 1 in dom r ; :: thesis:
hence [(r . j),(r . (j + 1))] in R by Z4, REWRITE1:def 2; :: thesis:
hence r . (j + 1) <> r . j by PREFER_1:22; :: thesis:

end;

A3: for i being Nat st i >= j + 1 & S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis:
assume Z5: ( i >= j + 1 & S₁[i] & i + 1 in dom r ) ; :: thesis:
then ( 1 <= j + 1 & i < i + 1 & i + 1 <= len r ) by NAT_1:11, NAT_1:13, FINSEQ_3:25;
then ( 1 <= i & i <= len r ) by Z5, XXREAL_0:2;
then i in dom r by FINSEQ_3:25;
then ZZ: ( [(r . j),(r . i)] in R & [(r . i),(r . (i + 1))] in R ) by Z5, REWRITE1:def 2;
hence [(r . j),(r . (i + 1))] in R by RELAT_2:31; :: thesis:
thus r . (i + 1) <> r . j by PREFER_1:22, ZZ; :: thesis:

end;

for i being Nat st i >= j + 1 holds
S₁[i] from NAT_1:sch 8(A2, A3);
hence r . i <> r . j by A1, Z3; :: thesis:

end;