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)
A3: now :: thesis: for b being Element of L st Y is_<=_than b holds
"\/" (X,L) <= b
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;
X is_<=_than "\/" (X,L) by A1, Def9;
then A4: Y is_<=_than "\/" (X,L) by A2;
ex_sup_of Y,L by A1, A2, Th46;
hence "\/" (X,L) = "\/" (Y,L) by A4, A3, Def9; :: thesis: verum