begin
definition
let U0 be
Universal_Algebra;
existence
ex b1 being BinOp of (Sub U0) st
for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 "\/" U2
uniqueness
for b1, b2 being BinOp of (Sub U0) st ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 "\/" U2 ) & ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b2 . (x,y) = U1 "\/" U2 ) holds
b1 = b2
end;
definition
let U0 be
Universal_Algebra;
existence
ex b1 being BinOp of (Sub U0) st
for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 /\ U2
uniqueness
for b1, b2 being BinOp of (Sub U0) st ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b2 . (x,y) = U1 /\ U2 ) holds
b1 = b2
end;