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 A6: x <= "\/" X,L by A5, LATTICE3:def 9;
"\/" X,L <= ("\/" X,L) "\/" ("\/" Y,L) by YELLOW_0:22;
hence x <= ("\/" X,L) "\/" ("\/" Y,L) by A6, ORDERS_2:26; :: thesis: verum

end;

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

Y is_<=_than "\/" Y,L by A2, YELLOW_0:30;
then A8: x <= "\/" Y,L by A7, LATTICE3:def 9;
"\/" Y,L <= ("\/" X,L) "\/" ("\/" Y,L) by YELLOW_0:22;
hence x <= ("\/" X,L) "\/" ("\/" Y,L) by A8, 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 A9: X \/ Y is_<=_than b ; :: thesis: ("\/" X,L) "\/" ("\/" Y,L) <= b
Y c= X \/ Y by XBOOLE_1:7;
then Y is_<=_than b by A9, YELLOW_0:9;
then A10: "\/" Y,L <= b by A2, YELLOW_0:30;
X c= X \/ Y by XBOOLE_1:7;
then X is_<=_than b by A9, YELLOW_0:9;
then "\/" X,L <= b by A1, YELLOW_0:30;
hence ("\/" X,L) "\/" ("\/" Y,L) <= b by A10, 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