environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, MARGREL1, PARTIT1, EQREL_1, FUNCT_1, SETFAM_1, RELAT_1, ZFMISC_1, TARSKI, RELAT_2, XBOOLEAN, BVFUNC_2, BVFUNC_1, FUNCT_4, FUNCT_5, OPOSET_1, BINOP_1, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, MARGREL1, RELAT_1, RELAT_2, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_5, EQREL_1, PARTIT1, BVFUNC_1, BVFUNC_2;
definitions BVFUNC_1, TARSKI, RELAT_2, XBOOLE_0, RELSET_1;
theorems TARSKI, FUNCT_1, FUNCT_2, BVFUNC_1, BVFUNC_2, RELSET_1, PARTIT1, SETFAM_1, SUBSET_1, FUNCT_4, RELAT_1, EQREL_1, RELAT_2, XBOOLE_0, XBOOLE_1, PARTFUN1, ORDERS_1, XBOOLEAN, MARGREL1, ZFMISC_1, XTUPLE_0;
schemes FUNCT_2;
registrations SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, EQREL_1, MARGREL1, PARTIT1, RELSET_1, XBOOLE_0, FUNCT_2;
constructors HIDDEN, SETFAM_1, FUNCT_4, XCMPLX_0, BVFUNC_1, BVFUNC_2, RELSET_1, FUNCT_5, RELAT_2, DOMAIN_1, BINOP_1, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, ARITHM, NUMERALS;
equalities XBOOLEAN, EQREL_1, ORDINAL1;
expansions BVFUNC_1, RELAT_2, XBOOLE_0;
Lm1:
for Y being non empty set
for G being Subset of (PARTITIONS Y) st G is independent holds
for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
theorem Th15:
for
Y being non
empty set for
a being
Function of
Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
P,
Q being
a_partition of
Y st
G is
independent holds
All (
(All (a,P,G)),
Q,
G)
= All (
(All (a,Q,G)),
P,
G)
theorem
for
Y being non
empty set for
a being
Function of
Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
P,
Q being
a_partition of
Y st
G is
independent holds
Ex (
(Ex (a,P,G)),
Q,
G)
= Ex (
(Ex (a,Q,G)),
P,
G)
theorem
for
Y being non
empty set for
a being
Function of
Y,
BOOLEAN for
G being
Subset of
(PARTITIONS Y) for
P,
Q being
a_partition of
Y st
G is
independent holds
Ex (
(All (a,P,G)),
Q,
G)
'<' All (
(Ex (a,Q,G)),
P,
G)