let L be RelStr ; :: thesis: for X being set
for x being Element of L holds
( x is_minimal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x > y ) ) ) )
let X be set ; :: thesis: for x being Element of L holds
( x is_minimal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x > y ) ) ) )
let x be Element of L; :: thesis: ( x is_minimal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x > y ) ) ) )

hereby :: thesis: ( x in X & ( for y being Element of L holds
( not y in X or not x > y ) ) implies x is_minimal_in X )

assume x is_minimal_in X ; :: thesis: ( x in X & ( for y being Element of L holds
( not b₂ in X or not x > b₂ ) ) )
then A1: x is_minimal_wrt X, the InternalRel of L ;
hence x in X ; :: thesis: for y being Element of L holds
( not b₂ in X or not x > b₂ )
let y be Element of L; :: thesis: ( not b₁ in X or not x > b₁ )

per cases ( not y in X or y = x or not [y,x] in the InternalRel of L ) by A1;

suppose not y in X ; :: thesis: ( not b₁ in X or not x > b₁ )

hence ( not y in X or not x > y ) ; :: thesis: verum

end;

suppose y = x ; :: thesis: ( not b₁ in X or not x > b₁ )

hence ( not y in X or not x > y ) ; :: thesis: verum

end;

suppose not [y,x] in the InternalRel of L ; :: thesis: ( not b₁ in X or not b₁ < x )

then not y <= x by ORDERS_2:def 5;
hence ( not y in X or not y < x ) by ORDERS_2:def 6; :: thesis: verum

end;

end;

end;

assume that
A2: x in X and
A3: for y being Element of L holds
( not y in X or not x > y ) ; :: thesis: x is_minimal_in X
assume not x is_minimal_in X ; :: thesis: contradiction
then not x is_minimal_wrt X, the InternalRel of L ;
then consider y being set such that
A4: y in X and
A5: y <> x and
A6: [y,x] in the InternalRel of L by A2;
reconsider y = y as Element of L by A6, ZFMISC_1:87;
y <= x by A6, ORDERS_2:def 5;
then y < x by A5, ORDERS_2:def 6;
hence contradiction by A3, A4; :: thesis: verum