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:3; :: 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:3; :: 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