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

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