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);