let L be transitive antisymmetric with_suprema RelStr ; 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 ; ( 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
; ( 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))
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;
( X \/ Y is_<=_than b implies ("\/" (X,L)) "\/" ("\/" (Y,L)) <= b )
assume A9:
X \/ Y is_<=_than b
;
("\/" (X,L)) "\/" ("\/" (Y,L)) <= b
Y c= X \/ Y
by XBOOLE_1:7;
then
Y is_<=_than b
by A9;
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;
then
"\/" (
X,
L)
<= b
by A1, YELLOW_0:30;
hence
("\/" (X,L)) "\/" ("\/" (Y,L)) <= b
by A10, YELLOW_0:22;
verum
end;
hence
( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) )
by A3, YELLOW_0:30; verum