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 )
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 #); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume that
A4: x <= y and
A5: y <= z ; :: thesis: 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; :: thesis: 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 #); :: according to YELLOW_0:def 3 :: thesis: ( not x <= y or not y <= x or x = y )
assume that
A8: x <= y and
A9: y <= x ; :: thesis: 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; :: thesis: 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 <> {} ; :: thesis: 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 ; :: thesis: x is_maximal_wrt X,R
thus x in X by A11; :: according to WAYBEL_4:def 23 :: 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 A13: y in X and
A14: y <> x and
A15: [x,y] in R ; :: thesis: contradiction
thus contradiction by A12, A13, A14, A15; :: thesis: verum