The abstract of the Mizar article:

Predicate Calculus for Boolean Valued Functions. Part VII

by

Shunichi Kobayashi

Received October 19, 1999

MML identifier: BVFUNC15

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, BVFUNC_2, T_1TOPSP, BOOLE,
      FUNCT_1, SETFAM_1, RELAT_1, CANTOR_1, CAT_1, FUNCT_4;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
      FRAENKEL, MARGREL1, SETFAM_1, EQREL_1, CANTOR_1, CQC_LANG, PARTIT1,
      BVFUNC_1, BVFUNC_2, FUNCT_4;
 constructors DOMAIN_1, AMI_1, CANTOR_1, BVFUNC_2, BVFUNC_1;
 clusters SUBSET_1, FUNCT_7, PARTIT1, MARGREL1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Predicate Calculus

theorem :: BVFUNC15:1
 for Y being non empty set,
     a being Element of Funcs(Y,BOOLEAN),
     G being Subset of PARTITIONS(Y),
     A,B,C being a_partition of Y, z,u being Element of Y
st G is independent & G={A,B,C} & A<>B & B<>C & C<>A &
EqClass(z,C)=EqClass(u,C)
holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G));