let R be non empty antisymmetric transitive Relation; for X being finite Subset of (field R) st X <> {} holds
ex x being Element of X st x is_maximal_wrt X,R
let X be finite Subset of (field R); ( X <> {} implies ex x being Element of X st x is_maximal_wrt X,R )
reconsider IR = R as Relation of (field R) by PRE_POLY:18;
set S = RelStr(# (field R),IR #);
set CR = the carrier of RelStr(# (field R),IR #);
set ir = the InternalRel of RelStr(# (field R),IR #);
A1:
not the carrier of RelStr(# (field R),IR #) is empty
;
A2:
R is_transitive_in field R
by RELAT_2:def 16;
A3:
RelStr(# (field R),IR #) is transitive
proof
let x,
y,
z be
Element of
RelStr(#
(field R),
IR #);
YELLOW_0:def 2 ( not x <= y or not y <= z or x <= z )
assume that A4:
x <= y
and A5:
y <= z
;
x <= z
A6:
[y,z] in the
InternalRel of
RelStr(#
(field R),
IR #)
by A5, ORDERS_2:def 5;
[x,y] in the
InternalRel of
RelStr(#
(field R),
IR #)
by A4, ORDERS_2:def 5;
then
[x,z] in the
InternalRel of
RelStr(#
(field R),
IR #)
by A1, A2, A6;
hence
x <= z
by ORDERS_2:def 5;
verum
end;
A7:
R is_antisymmetric_in field R
by RELAT_2:def 12;
RelStr(# (field R),IR #) is antisymmetric
proof
let x,
y be
Element of
RelStr(#
(field R),
IR #);
YELLOW_0:def 3 ( not x <= y or not y <= x or x = y )
assume that A8:
x <= y
and A9:
y <= x
;
x = y
A10:
[y,x] in the
InternalRel of
RelStr(#
(field R),
IR #)
by A9, ORDERS_2:def 5;
[x,y] in the
InternalRel of
RelStr(#
(field R),
IR #)
by A8, ORDERS_2:def 5;
hence
x = y
by A1, A7, A10;
verum
end;
then reconsider S = RelStr(# (field R),IR #) as non empty transitive antisymmetric RelStr by A3;
reconsider Y = X as finite Subset of the carrier of RelStr(# (field R),IR #) ;
assume
X <> {}
; ex x being Element of X st x is_maximal_wrt X,R
then consider x being Element of S such that
A11:
x in Y
and
A12:
x is_maximal_wrt Y, the InternalRel of S
by BAGORDER:6;
reconsider x = x as Element of X by A11;
take
x
; x is_maximal_wrt X,R
thus
x in X
by A11; WAYBEL_4:def 23 for b1 being set holds
( not b1 in X or b1 = x or not [x,b1] in R )
given y being set such that A13:
y in X
and
A14:
y <> x
and
A15:
[x,y] in R
; contradiction
thus
contradiction
by A12, A13, A14, A15; verum