environ
vocabularies HIDDEN, NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_2, TARSKI, UNIALG_1, FUNCT_2, PARTFUN1, RELAT_1, FINSEQ_1, FUNCOP_1, STRUCT_0, CQC_SIM1, FUNCT_1, CARD_1, ZFMISC_1, SETFAM_1, EQREL_1, BINOP_1, LATTICES, UNIALG_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1, SETFAM_1, FUNCOP_1, PARTFUN1, FINSEQ_2, LATTICES, BINOP_1, UNIALG_1, MARGREL1;
definitions TARSKI, XBOOLE_0, MARGREL1;
theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, UNIALG_1, ZFMISC_1, SETFAM_1, FUNCOP_1, BINOP_1, LATTICES, FINSEQ_3, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, MARGREL1;
schemes FINSEQ_1, BINOP_1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, FINSEQ_2, STRUCT_0, LATTICES, UNIALG_1, ORDINAL1, FINSEQ_1, CARD_1, MARGREL1;
constructors HIDDEN, SETFAM_1, BINOP_1, DOMAIN_1, FUNCOP_1, LATTICES, UNIALG_1, MARGREL1, FINSEQ_2, RELSET_1, NUMBERS;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities SUBSET_1, FUNCOP_1;
expansions TARSKI, XBOOLE_0, MARGREL1;
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;