let R be non empty transitive asymmetric RelStr ; :: thesis:
let X be set ; :: thesis:
assume X is finite ; :: thesis:
then reconsider X1 = X as finite set ;
given x being Element of R such that Z1: x in X ; :: thesis:
set Y = { r where r is Element of X1 * : r is RedSequence of the InternalRel of R } ;
defpred S₁[ Nat] means ex r being RedSequence of the InternalRel of R st
( r in { r where r is Element of X1 * : r is RedSequence of the InternalRel of R } & len r = $1 );
A1: for k being Nat st S₁[k] holds
k <= card X1

let k be Nat; :: thesis:
given r being RedSequence of the InternalRel of R such that A2: ( r in { r where r is Element of X1 * : r is RedSequence of the InternalRel of R } & len r = k ) ; :: thesis:
consider q being Element of X1 * such that
A3: ( r = q & q is RedSequence of the InternalRel of R ) by A2;
( rng r c= X1 & r is one-to-one ) by A3, Th13, FINSEQ_1:def 4;
then ( len r = card (rng r) & card (rng r) <= card X1 ) by PRE_POLY:19, NAT_1:43;
hence k <= card X1 by A2; :: thesis:

end;

set k = 1;
reconsider r = <*x*> as RedSequence of the InternalRel of R by REWRITE1:6;
take r ; :: thesis:
<*x*> is FinSequence of X1 by Z1, FINSEQ_1:74;
then <*x*> in X1 * by FINSEQ_1:def 11;
hence r in { r where r is Element of X1 * : r is RedSequence of the InternalRel of R } ; :: thesis:
thus len r = 1 by FINSEQ_1:39; :: thesis:

end;

then A4: ex k being Nat st S₁[k] ;
consider k being Nat such that
A5: ( S₁[k] & ( for n being Nat st S₁[n] holds
n <= k ) ) from NAT_1:sch 6(A1, A4);
consider r being RedSequence of the InternalRel of R such that
A6: ( r in { r where r is Element of X1 * : r is RedSequence of the InternalRel of R } & len r = k ) by A5;
consider q being Element of X1 * such that
A7: ( r = q & q is RedSequence of the InternalRel of R ) by A6;
1 <= k by B1, A5;

take x ; :: thesis:
for y being Element of R holds
( not y in X or not x < y )

given y being Element of R such that A8: ( y in X & x < y ) ; :: thesis:
[x,y] in the InternalRel of R by A8, ORDERS_2:def 5, ORDERS_2:def 6;
then reconsider r = <*x,y*> as RedSequence of the InternalRel of R by REWRITE1:7;
<*x,y*> is FinSequence of X1 by Z1, A8, FINSEQ_2:13;
then r in X1 * by FINSEQ_1:def 11;
then ( r in { r where r is Element of X1 * : r is RedSequence of the InternalRel of R } & len r = 2 ) by FINSEQ_1:44;
hence contradiction by A5, C1; :: thesis:

end;

end;

then reconsider x = r . k as Element of R by A6, Lem5;
take x ; :: thesis:
A9: ( k in dom r & r is FinSequence of X1 ) by A6, A7, FINSEQ_5:6;
for y being Element of R holds
( not y in X or not x < y )

given y being Element of R such that B1: ( y in X & x < y ) ; :: thesis:
[x,y] in the InternalRel of R by B1, ORDERS_2:def 5, ORDERS_2:def 6;
then reconsider p = <*x,y*> as RedSequence of the InternalRel of R by REWRITE1:7;
p . 1 = x by FINSEQ_1:44;
then reconsider rp = r $^ p as RedSequence of the InternalRel of R by A6, REWRITE1:8;
ex i being Nat st k = 1 + i by A8, NAT_1:10;
then consider t being FinSequence, a being object such that
B2: r = t ^ <*a*> by A6, FINSEQ_2:18;
k = (len t) + 1 by A6, B2, FINSEQ_2:16;
then x = a by B2, FINSEQ_1:42;
then B3: rp = r ^ <*y*> by B2, REWRITE1:3;
reconsider yy = <*y*>, r1 = r as FinSequence of X1 by A7, B1, FINSEQ_1:74;
r1 ^ yy is FinSequence of X1 ;
then rp in X1 * by B3, FINSEQ_1:def 11;
then ( rp in { r where r is Element of X1 * : r is RedSequence of the InternalRel of R } & len rp = k + 1 ) by A6, B3, FINSEQ_2:16;
then k + 1 <= k by A5;
hence contradiction by NAT_1:13; :: thesis:

end;

end;