let R be non empty transitive asymmetric RelStr ; :: thesis: for X being set st X is finite & ex x being Element of R st x in X holds
ex x being Element of R st x is_maximal_in X
let X be set ; :: thesis: ( X is finite & ex x being Element of R st x in X implies ex x being Element of R st x is_maximal_in X )
assume X is finite ; :: thesis: ( for x being Element of R holds not x in X or ex x being Element of R st x is_maximal_in X )
then reconsider X1 = X as finite set ;
given x being Element of R such that Z1: x in X ; :: thesis: ex x being Element of R st x is_maximal_in X
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

proof

let k be Nat; :: thesis: ( S₁[k] implies k <= card X1 )
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: k <= card X1
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: verum

end;

B1: S₁[1]

proof

set k = 1;
reconsider r = <*x*> as RedSequence of the InternalRel of R by REWRITE1:6;
take r ; :: thesis: ( r in { r where r is Element of X1 * : r is RedSequence of the InternalRel of R } & len r = 1 )
<*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: len r = 1
thus len r = 1 by FINSEQ_1:39; :: thesis: verum

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;

per cases then ( k = 1 or k > 1 ) by XXREAL_0:1;

suppose C1: k = 1 ; :: thesis: ex x being Element of R st x is_maximal_in X

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

proof

given y being Element of R such that A8: ( y in X & x < y ) ; :: thesis: contradiction
[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: verum

end;

hence x is_maximal_in X by Z1, WAYBEL_4:55; :: thesis: verum

end;

suppose A8: k > 1 ; :: thesis: ex x being Element of R st x is_maximal_in X

then reconsider x = r . k as Element of R by A6, Lem5;
take x ; :: thesis: x is_maximal_in X
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 )

proof

given y being Element of R such that B1: ( y in X & x < y ) ; :: thesis: contradiction
[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 ;
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: verum

end;

hence x is_maximal_in X by A9, FUNCT_1:102, WAYBEL_4:55; :: thesis: verum

end;

end;