environ
vocabularies HIDDEN, FUNCT_1, PBOOLE, RELAT_1, FUNCT_4, FUNCOP_1, XBOOLE_0, FINSET_1, TARSKI, ZFMISC_1, PZFMISC1, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_4, FINSET_1, FUNCOP_1, PBOOLE, MBOOLEAN;
definitions FINSET_1, PBOOLE;
theorems FUNCOP_1, ENUMSET1, FUNCT_4, MBOOLEAN, PBOOLE, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0, PARTFUN1;
schemes PBOOLE;
registrations XBOOLE_0, FUNCOP_1, FINSET_1;
constructors HIDDEN, FUNCT_4, MBOOLEAN, PBOOLE, FINSET_1, RELSET_1;
requirements HIDDEN, BOOLE;
equalities FUNCOP_1;
expansions PBOOLE;
theorem
for
I being
set for
x,
y,
X being
ManySortedSet of
I holds
(
[|{x,y},X|] = [|{x},X|] (\/) [|{y},X|] &
[|X,{x,y}|] = [|X,{x}|] (\/) [|X,{y}|] )