let R be non empty transitive antisymmetric with_finite_clique# RelStr ; :: thesis: for x being Element of R ex y being Element of R st
( y is_minimal_in [#] R & ( y = x or y < x ) )
let x be Element of R; :: thesis: ex y being Element of R st
( y is_minimal_in [#] R & ( y = x or y < x ) )
set sx = Lower {x};
set sL = subrelstr (Lower {x});
reconsider sL = subrelstr (Lower {x}) as non empty transitive antisymmetric with_finite_clique# RelStr ;
consider y being set such that
A: y in minimals sL by XBOOLE_0:def 1;
reconsider y = y as Element of sL by A;
C: [#] sL = Lower {x} by YELLOW_0:def 15;
then B: y is_minimal_in Lower {x} by A, Lmin;
reconsider y9 = y as Element of R by YELLOW_0:59;
take y9 ; :: thesis: ( y9 is_minimal_in [#] R & ( y9 = x or y9 < x ) )
Lower {x} c= the carrier of sL by YELLOW_0:def 15;
hence y9 is_minimal_in [#] R by B, SPmin, Pminmin; :: thesis: ( y9 = x or y9 < x )

per cases ( y9 = x or y9 <> x ) ;

suppose y9 = x ; :: thesis: ( y9 = x or y9 < x )

hence ( y9 = x or y9 < x ) ; :: thesis: verum

end;

suppose y9 <> x ; :: thesis: ( y9 = x or y9 < x )

then not y9 in {x} by TARSKI:def 1;
then y9 in downarrow x by XBOOLE_0:def 3, C;
then y9 <= x by WAYBEL_0:17;
hence ( y9 = x or y9 < x ) by ORDERS_2:def 10; :: thesis: verum

end;

end;