The abstract of the Mizar article:

Predicate Calculus for Boolean Valued Functions. Part X

by

Shunichi Kobayashi

Received November 15, 1999

MML identifier: BVFUNC18

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, BVFUNC_2, ZF_LANG, BVFUNC_1,
      T_1TOPSP;
 notation XBOOLE_0, SUBSET_1, FRAENKEL, MARGREL1, VALUAT_1, EQREL_1, SETWISEO,
      BVFUNC_1, BVFUNC_2;
 constructors SETWISEO, BVFUNC_2, BVFUNC_1;
 clusters SUBSET_1, MARGREL1, VALUAT_1, AMI_1, XBOOLE_0;


begin :: Chap. 1  Predicate Calculus

reserve Y for non empty set;

canceled 3;

theorem :: BVFUNC18:4
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B,C being a_partition of Y holds
All('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G);

canceled 2;

theorem :: BVFUNC18:7
for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C being a_partition of Y
st G is independent & G={A,B,C} & A<>B & B<>C & C<>A holds
Ex('not' All(a,A,G),B,G) = Ex('not' All(a,B,G),A,G);

canceled 6;

theorem :: BVFUNC18:14
for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C being a_partition of Y
st G is independent & G={A,B,C} & A<>B & B<>C & C<>A holds
All('not' Ex(a,A,G),B,G) = All('not' Ex(a,B,G),A,G);