let R be transitive RelStr ; :: thesis: for x being Element of R
for S being Subset of R st x is_minimal_in Lower S holds
x is_minimal_in [#] R
let x be Element of R; :: thesis: for S being Subset of R st x is_minimal_in Lower S holds
x is_minimal_in [#] R
let S be Subset of R; :: thesis: ( x is_minimal_in Lower S implies x is_minimal_in [#] R )
assume A: x is_minimal_in Lower S ; :: thesis: x is_minimal_in [#] R
set cR = the carrier of R;
B: x in Lower S by A, WAYBEL_4:57;
assume not x is_minimal_in [#] R ; :: thesis: contradiction
then consider y being Element of R such that
y in the carrier of R and
E: y < x by B, WAYBEL_4:57;

per cases ( x in S or x in downarrow S ) by B, XBOOLE_0:def 3;

suppose S1: x in S ; :: thesis: contradiction

y <= x by E, ORDERS_2:def 10;
then y in downarrow S by S1, WAYBEL_0:def 15;
then y in Lower S by XBOOLE_0:def 3;
hence contradiction by A, E, WAYBEL_4:57; :: thesis: verum

end;

suppose x in downarrow S ; :: thesis: contradiction

then consider x99 being Element of R such that
H: x <= x99 and
I: x99 in S by WAYBEL_0:def 15;
y <= x by E, ORDERS_2:def 10;
then y <= x99 by H, YELLOW_0:def 2;
then y in downarrow S by I, WAYBEL_0:def 15;
then y in Lower S by XBOOLE_0:def 3;
hence contradiction by A, E, WAYBEL_4:57; :: thesis: verum

end;

end;