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 cR = the carrier of R;
set iR = the InternalRel of R;
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;
B: y is_minimal_in Lower {x} by A, C, Lmin;
reconsider y' = y as Element of R by YELLOW_0:59;
take y' ; :: thesis: ( y' is_minimal_in [#] R & ( y' = x or y' < x ) )
Lower {x} c= the carrier of sL by YELLOW_0:def 15;
hence y' is_minimal_in [#] R by B, SPmin, Pminmin; :: thesis: ( y' = x or y' < x )

per cases ( y' = x or y' <> x ) ;

suppose y' = x ; :: thesis: ( y' = x or y' < x )

hence ( y' = x or y' < x ) ; :: thesis: verum

end;

suppose y' <> x ; :: thesis: ( y' = x or y' < x )

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

end;

end;