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

proof

let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in X \/ Y or x <= ("\/" X,L) "\/" ("\/" Y,L) )
assume A4: x in X \/ Y ; :: thesis: x <= ("\/" X,L) "\/" ("\/" Y,L)

per cases ( x in X or x in Y ) by A4, XBOOLE_0:def 3;

suppose A5: x in X ; :: thesis: x <= ("\/" X,L) "\/" ("\/" Y,L)

X is_<=_than "\/" X,L by A1, YELLOW_0:30;
then ( x <= "\/" X,L & "\/" X,L <= ("\/" X,L) "\/" ("\/" Y,L) ) by A5, LATTICE3:def 9, YELLOW_0:22;
hence x <= ("\/" X,L) "\/" ("\/" Y,L) by ORDERS_2:26; :: thesis: verum

end;

suppose A6: x in Y ; :: thesis: x <= ("\/" X,L) "\/" ("\/" Y,L)

Y is_<=_than "\/" Y,L by A2, YELLOW_0:30;
then ( x <= "\/" Y,L & "\/" Y,L <= ("\/" X,L) "\/" ("\/" Y,L) ) by A6, LATTICE3:def 9, YELLOW_0:22;
hence x <= ("\/" X,L) "\/" ("\/" Y,L) by ORDERS_2:26; :: thesis: verum

end;

end;

end;

for b being Element of L st X \/ Y is_<=_than b holds
("\/" X,L) "\/" ("\/" Y,L) <= b

proof

let b be Element of L; :: thesis: ( X \/ Y is_<=_than b implies ("\/" X,L) "\/" ("\/" Y,L) <= b )
assume A7: X \/ Y is_<=_than b ; :: thesis: ("\/" X,L) "\/" ("\/" Y,L) <= b
( X c= X \/ Y & Y c= X \/ Y ) by XBOOLE_1:7;
then ( X is_<=_than b & Y is_<=_than b ) by A7, YELLOW_0:9;
then ( "\/" X,L <= b & "\/" Y,L <= b ) by A1, A2, YELLOW_0:30;
hence ("\/" X,L) "\/" ("\/" Y,L) <= b by YELLOW_0:22; :: thesis: verum

end;

hence ( ex_sup_of X \/ Y,L & "\/" (X \/ Y),L = ("\/" X,L) "\/" ("\/" Y,L) ) by A3, YELLOW_0:30; :: thesis: verum