let L be transitive antisymmetric RelStr ; :: thesis: for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L & ex_sup_of X \/ Y,L holds
"\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L))
let X, Y be set ; :: thesis: ( ex_sup_of X,L & ex_sup_of Y,L & ex_sup_of X \/ Y,L implies "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) )
assume that
A1: ( ex_sup_of X,L & ex_sup_of Y,L ) and
A2: ex_sup_of X \/ Y,L ; :: thesis: "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L))
set a = "\/" (X,L);
set b = "\/" (Y,L);
set c = "\/" ((X \/ Y),L);
A3: ( "\/" (X,L) is_>=_than X & "\/" (Y,L) is_>=_than Y ) by A1, Th30;

A4: now :: thesis: for d being Element of L st d >= "\/" (X,L) & d >= "\/" (Y,L) holds
"\/" ((X \/ Y),L) <= d

let d be Element of L; :: thesis: ( d >= "\/" (X,L) & d >= "\/" (Y,L) implies "\/" ((X \/ Y),L) <= d )
assume ( d >= "\/" (X,L) & d >= "\/" (Y,L) ) ; :: thesis: "\/" ((X \/ Y),L) <= d
then ( d is_>=_than X & d is_>=_than Y ) by A3, Th4;
then d is_>=_than X \/ Y by Th10;
hence "\/" ((X \/ Y),L) <= d by A2, Th30; :: thesis: verum

end;

( "\/" ((X \/ Y),L) >= "\/" (X,L) & "\/" ((X \/ Y),L) >= "\/" (Y,L) ) by A1, A2, Th34, XBOOLE_1:7;
hence "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) by A4, Th18; :: thesis: verum