let R be transitive RelStr ; :: thesis: for x being Element of R
for S being Subset of R st x is_maximal_in Upper S holds
x is_maximal_in [#] R
let x be Element of R; :: thesis: for S being Subset of R st x is_maximal_in Upper S holds
x is_maximal_in [#] R
let S be Subset of R; :: thesis: ( x is_maximal_in Upper S implies x is_maximal_in [#] R )
assume A1: x is_maximal_in Upper S ; :: thesis: x is_maximal_in [#] R
set cR = the carrier of R;
A2: x in Upper S by A1, WAYBEL_4:55;
assume not x is_maximal_in [#] R ; :: thesis: contradiction
then consider y being Element of R such that
y in the carrier of R and
A3: x < y by A2, WAYBEL_4:55;

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

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

x <= y by A3;
then y in uparrow S by A4, WAYBEL_0:def 16;
then y in Upper S by XBOOLE_0:def 3;
hence contradiction by A1, A3, WAYBEL_4:55; :: thesis: verum

end;

suppose x in uparrow S ; :: thesis: contradiction

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

end;

end;