let R be non empty transitive asymmetric RelStr ; 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 ; ( 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
; ( 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
; 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 S1[ 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 S1[k] holds
k <= card X1
B1:
S1[1]
then A4:
ex k being Nat st S1[k]
;
consider k being Nat such that
A5:
( S1[k] & ( for n being Nat st S1[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 A8:
k > 1
;
ex x being Element of R st x is_maximal_in Xthen reconsider x =
r . k as
Element of
R by A6, Lem5;
take
x
;
x is_maximal_in XA9:
(
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 )
;
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
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;
verum
end; hence
x is_maximal_in X
by A9, FUNCT_1:102, WAYBEL_4:55;
verum end; end;