environ
vocabularies HIDDEN, FUNCT_1, RELAT_1, SETFAM_1, XBOOLE_0, SUBSET_1, PARTFUN1, FUNCOP_1, TARSKI, FUNCT_2, ZFMISC_1, MEMBER_1, FUNCT_4, PBOOLE, NAT_1, SETLIM_2;
notations HIDDEN, TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1;
theorems TARSKI, FUNCOP_1, FUNCT_1, RELAT_1, XBOOLE_0, XBOOLE_1, FUNCT_2, PARTFUN1, FUNCT_4, ZFMISC_1, SETFAM_1;
schemes FUNCT_1, CLASSES1, XBOOLE_0;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FUNCT_4, RELAT_1;
constructors HIDDEN, SETFAM_1, FUNCOP_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_4;
requirements HIDDEN, BOOLE, SUBSET;
equalities XBOOLE_0;
expansions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1;
definition
let I be
set ;
coherence
I --> {} is ManySortedSet of I
;
correctness
;
let X,
Y be
ManySortedSet of
I;
existence
ex b1 being ManySortedSet of I st
for i being object st i in I holds
b1 . i = (X . i) \/ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being object st i in I holds
b1 . i = (X . i) \/ (Y . i) ) & ( for i being object st i in I holds
b2 . i = (X . i) \/ (Y . i) ) holds
b1 = b2
commutativity
for b1, X, Y being ManySortedSet of I st ( for i being object st i in I holds
b1 . i = (X . i) \/ (Y . i) ) holds
for i being object st i in I holds
b1 . i = (Y . i) \/ (X . i)
;
idempotence
for X being ManySortedSet of I
for i being object st i in I holds
X . i = (X . i) \/ (X . i)
;
existence
ex b1 being ManySortedSet of I st
for i being object st i in I holds
b1 . i = (X . i) /\ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being object st i in I holds
b1 . i = (X . i) /\ (Y . i) ) & ( for i being object st i in I holds
b2 . i = (X . i) /\ (Y . i) ) holds
b1 = b2
commutativity
for b1, X, Y being ManySortedSet of I st ( for i being object st i in I holds
b1 . i = (X . i) /\ (Y . i) ) holds
for i being object st i in I holds
b1 . i = (Y . i) /\ (X . i)
;
idempotence
for X being ManySortedSet of I
for i being object st i in I holds
X . i = (X . i) /\ (X . i)
;
existence
ex b1 being ManySortedSet of I st
for i being object st i in I holds
b1 . i = (X . i) \ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being object st i in I holds
b1 . i = (X . i) \ (Y . i) ) & ( for i being object st i in I holds
b2 . i = (X . i) \ (Y . i) ) holds
b1 = b2
symmetry
for X, Y being ManySortedSet of I st ( for i being object st i in I holds
X . i meets Y . i ) holds
for i being object st i in I holds
Y . i meets X . i
;
symmetry
for X, Y being ManySortedSet of I st ( for i being object st i in I holds
X . i misses Y . i ) holds
for i being object st i in I holds
Y . i misses X . i
;
end;
Lm1:
for I being set
for X, Y being ManySortedSet of I st X c= Y & Y c= X holds
X = Y