environ
vocabularies HIDDEN, XBOOLE_0, ORDERS_2, OSALG_1, PBOOLE, SUBSET_1, XXREAL_0, FUNCT_1, TARSKI, RELAT_1, MSUALG_1, MSUALG_2, SEQM_3, STRUCT_0, UNIALG_2, CARD_3, ZFMISC_1, QC_LANG1, SETFAM_1, BINOP_1, LATTICES, EQREL_1, XXREAL_2, OSALG_2, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, SETFAM_1, BINOP_1, CARD_3, MBOOLEAN, PBOOLE, FINSEQ_2, STRUCT_0, LATTICES, MSUALG_1, ORDERS_2, MSUALG_2, OSALG_1;
definitions TARSKI, PBOOLE, LATTICES, OSALG_1, MSUALG_2;
theorems TARSKI, XBOOLE_0, XBOOLE_1, FUNCT_1, PBOOLE, CARD_3, MSUALG_1, FUNCT_2, ZFMISC_1, SETFAM_1, BINOP_1, LATTICES, RELAT_1, OSALG_1, ORDERS_2, MSUALG_2, MBOOLEAN, PARTFUN1;
schemes XBOOLE_0, BINOP_1, FUNCT_1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, MSUALG_1, MSUALG_2, ORDERS_3, OSALG_1, FUNCT_1, RELAT_1, PBOOLE, FINSEQ_1;
constructors HIDDEN, SETFAM_1, MBOOLEAN, MSUALG_2, ORDERS_3, OSALG_1, RELSET_1, CARD_3;
requirements HIDDEN, BOOLE, SUBSET;
equalities LATTICES, MSUALG_2;
expansions TARSKI, PBOOLE, LATTICES, MSUALG_2;
definition
let S1 be
OrderSortedSign;
let U0 be
non-empty OSAlgebra of
S1;
existence
ex b1 being BinOp of (OSSub U0) st
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 "\/"_os U2
uniqueness
for b1, b2 being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 "\/"_os U2 ) & ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . (x,y) = U1 "\/"_os U2 ) holds
b1 = b2
end;
definition
let S1 be
OrderSortedSign;
let U0 be
non-empty OSAlgebra of
S1;
existence
ex b1 being BinOp of (OSSub U0) st
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 /\ U2
uniqueness
for b1, b2 being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b2 . (x,y) = U1 /\ U2 ) holds
b1 = b2
end;