let L be non empty RelStr ; :: thesis: for X, Y being set st ex_sup_of X,L & ( for x being Element of L holds
( x is_>=_than X iff x is_>=_than Y ) ) holds
"\/" X,L = "\/" Y,L
let X, Y be set ; :: thesis: ( ex_sup_of X,L & ( for x being Element of L holds
( x is_>=_than X iff x is_>=_than Y ) ) implies "\/" X,L = "\/" Y,L )
assume A1: ex_sup_of X,L ; :: thesis: ( ex x being Element of L st
( ( x is_>=_than X implies x is_>=_than Y ) implies ( x is_>=_than Y & not x is_>=_than X ) ) or "\/" X,L = "\/" Y,L )
assume A2: for x being Element of L holds
( x is_>=_than X iff x is_>=_than Y ) ; :: thesis: "\/" X,L = "\/" Y,L
then A3: ex_sup_of Y,L by A1, Th46;
X is_<=_than "\/" X,L by A1, Def9;
then A4: Y is_<=_than "\/" X,L by A2;

now

let b be Element of L; :: thesis: ( Y is_<=_than b implies "\/" X,L <= b )
assume Y is_<=_than b ; :: thesis: "\/" X,L <= b
then X is_<=_than b by A2;
hence "\/" X,L <= b by A1, Def9; :: thesis: verum

end;

hence "\/" X,L = "\/" Y,L by A3, A4, Def9; :: thesis: verum