The abstract of the Mizar article:

Four Variable Predicate Calculus for Boolean Valued Functions. Part II

by

Shunichi Kobayashi

Received November 26, 1999

MML identifier: BVFUNC21

[ Mizar article, MML identifier index ]

environ

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


begin :: Chap. 1  Four Variable Predicate Calculus

reserve Y for non empty set,
        a for Element of Funcs(Y,BOOLEAN),
        G for Subset of PARTITIONS(Y),
        A, B for a_partition of Y;

canceled 3;

theorem :: BVFUNC21:4
 All('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G);