let L be non empty RelStr ; :: thesis: for X, Y being set st ( for x being Element of L holds
( x is_>=_than X iff x is_>=_than Y ) ) & ex_sup_of X,L holds
ex_sup_of Y,L
let X, Y be set ; :: thesis: ( ( for x being Element of L holds
( x is_>=_than X iff x is_>=_than Y ) ) & ex_sup_of X,L implies ex_sup_of Y,L )
assume A1: for x being Element of L holds
( x is_>=_than X iff x is_>=_than Y ) ; :: thesis: ( not ex_sup_of X,L or ex_sup_of Y,L )
given a being Element of L such that A2: X is_<=_than a and
A3: for b being Element of L st X is_<=_than b holds
a <= b and
A4: for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds
c <= b ) holds
c = a ; :: according to YELLOW_0:def 7 :: thesis: ex_sup_of Y,L
take a ; :: according to YELLOW_0:def 7 :: thesis: ( Y is_<=_than a & ( for b being Element of L st Y is_<=_than b holds
b >= a ) & ( for c being Element of L st Y is_<=_than c & ( for b being Element of L st Y is_<=_than b holds
b >= c ) holds
c = a ) )
thus Y is_<=_than a by A1, A2; :: thesis: ( ( for b being Element of L st Y is_<=_than b holds
b >= a ) & ( for c being Element of L st Y is_<=_than c & ( for b being Element of L st Y is_<=_than b holds
b >= c ) holds
c = a ) )

hereby :: thesis: for c being Element of L st Y is_<=_than c & ( for b being Element of L st Y is_<=_than b holds
b >= c ) holds
c = a

let b be Element of L; :: thesis: ( Y is_<=_than b implies a <= b )
assume Y is_<=_than b ; :: thesis: a <= b
then X is_<=_than b by A1;
hence a <= b by A3; :: thesis: verum

end;

let c be Element of L; :: thesis: ( Y is_<=_than c & ( for b being Element of L st Y is_<=_than b holds
b >= c ) implies c = a )
assume A5: Y is_<=_than c ; :: thesis: ( ex b being Element of L st
( Y is_<=_than b & not b >= c ) or c = a )
assume A6: for b being Element of L st Y is_<=_than b holds
c <= b ; :: thesis: c = a

A7: now

let b be Element of L; :: thesis: ( X is_<=_than b implies c <= b )
assume X is_<=_than b ; :: thesis: c <= b
then Y is_<=_than b by A1;
hence c <= b by A6; :: thesis: verum

end;

X is_<=_than c by A1, A5;
hence c = a by A4, A7; :: thesis: verum