let R be non empty antisymmetric transitive Relation; :: thesis: 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); :: thesis: ( X <> {} implies ex x being Element of X st x is_maximal_wrt X,R )
assume A1: X <> {} ; :: thesis: ex x being Element of X st x is_maximal_wrt X,R
reconsider IR = R as Relation of (field R) by POLYNOM1:4;
set S = RelStr(# (field R),IR #);
set CR = the carrier of RelStr(# (field R),IR #);
set ir = the InternalRel of RelStr(# (field R),IR #);
A2: the carrier of RelStr(# (field R),IR #) is (C1) ;
A3: R is_antisymmetric_in field R by RELAT_2:def 12;
A4: RelStr(# (field R),IR #) is antisymmetric

proof

let x, y be Element of RelStr(# (field R),IR #); :: according to YELLOW_0:def 3 :: thesis: ( not x <= y or not y <= x or x = y )
assume ( x <= y & y <= x ) ; :: thesis: x = y
then ( [x,y] in the InternalRel of RelStr(# (field R),IR #) & [y,x] in the InternalRel of RelStr(# (field R),IR #) ) by ORDERS_2:def 9;
hence x = y by A2, A3, RELAT_2:def 4; :: thesis: verum

end;

A5: R is_transitive_in field R by RELAT_2:def 16;
RelStr(# (field R),IR #) is transitive

proof

let x, y, z be Element of RelStr(# (field R),IR #); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume ( x <= y & y <= z ) ; :: thesis: x <= z
then ( [x,y] in the InternalRel of RelStr(# (field R),IR #) & [y,z] in the InternalRel of RelStr(# (field R),IR #) ) by ORDERS_2:def 9;
then [x,z] in the InternalRel of RelStr(# (field R),IR #) by A2, A5, RELAT_2:def 8;
hence x <= z by ORDERS_2:def 9; :: thesis: verum

end;

then reconsider S = RelStr(# (field R),IR #) as non empty transitive antisymmetric RelStr by A2, A4;
reconsider Y = X as finite Subset of the carrier of RelStr(# (field R),IR #) ;
consider x being Element of S such that
A6: ( x in Y & x is_maximal_wrt Y,the InternalRel of S ) by A1, BAGORDER:7;
reconsider x = x as Element of X by A6;
take x ; :: thesis: x is_maximal_wrt X,R
thus x in X by A6; :: according to WAYBEL_4:def 24 :: thesis: for b₁ being set holds
( not b₁ in X or b₁ = x or not [x,b₁] in R )
given y being set such that A7: ( y in X & y <> x & [x,y] in R ) ; :: thesis: contradiction
thus contradiction by A6, A7, WAYBEL_4:def 24; :: thesis: verum