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 A: x is_maximal_in Upper S ; :: thesis: x is_maximal_in [#] R
set cR = the carrier of R;
B: x in Upper S by A, WAYBEL_4:56;
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
E: x < y by B, WAYBEL_4:56;

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

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

x <= y by E, ORDERS_2:def 10;
then y in uparrow S by S1, WAYBEL_0:def 16;
then y in Upper S by XBOOLE_0:def 3;
hence contradiction by A, E, WAYBEL_4:56; :: thesis: verum

end;

suppose x in uparrow S ; :: thesis: contradiction

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

end;

end;