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 A1: x is_minimal_in Lower S ; :: thesis: x is_minimal_in [#] R
set cR = the carrier of R;
A2: x in Lower S by A1, WAYBEL_4:56;
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
A3: y < x by A2, WAYBEL_4:56;

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

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

y <= x by A3;
then y in downarrow S by A4, WAYBEL_0:def 15;
then y in Lower S by XBOOLE_0:def 3;
hence contradiction by A1, A3, WAYBEL_4:56; :: thesis: verum

end;

suppose x in downarrow S ; :: thesis: contradiction

then consider x99 being Element of R such that
A5: x <= x99 and
A6: x99 in S by WAYBEL_0:def 15;
y <= x by A3;
then y <= x99 by A5, YELLOW_0:def 2;
then y in downarrow S by A6, WAYBEL_0:def 15;
then y in Lower S by XBOOLE_0:def 3;
hence contradiction by A1, A3, WAYBEL_4:56; :: thesis: verum

end;

end;