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 by Def27;
hence x in X by Def26; :: 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, Def26;

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 9;
hence ( not y in X or not y < x ) by ORDERS_2:def 10; :: thesis: verum

end;

end;

end;

assume A2: ( x in X & ( 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 by Def27;
then consider y being set such that
A3: ( y in X & y <> x & [y,x] in the InternalRel of L ) by A2, Def26;
reconsider y = y as Element of L by A3, ZFMISC_1:106;
y <= x by A3, ORDERS_2:def 9;
then y < x by A3, ORDERS_2:def 10;
hence contradiction by A2, A3; :: thesis: verum