The Mizar article BVFUNC21

The Mizar article:
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;
 definitions BVFUNC_1;
 theorems T_1TOPSP, MARGREL1, BVFUNC_1, BVFUNC_2, VALUAT_1;

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
 All('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G)
proof
    let z be Element of Y;
    assume A1:Pj(All('not' Ex(a,A,G),B,G),z)=TRUE;
A2:z in EqClass(z,CompF(B,G)) &
      EqClass(z,CompF(B,G)) in CompF(B,G)
      by T_1TOPSP:def 1;
    now assume
      not (for x being Element of Y st x in EqClass(z,CompF(B,G)) holds
       Pj('not' Ex(a,A,G),x)=TRUE);then
      Pj(B_INF('not' Ex(a,A,G),CompF(B,G)),z) = FALSE by BVFUNC_1:def 19;then
      Pj(All('not' Ex(a,A,G),B,G),z)=FALSE by BVFUNC_2:def 9;
      hence contradiction by A1,MARGREL1:43;
    end;then
    Pj('not' Ex(a,A,G),z)=TRUE by A2;then
    'not' Pj(Ex(a,A,G),z)=TRUE by VALUAT_1:def 5;then
    A3:Pj(Ex(a,A,G),z)=FALSE by MARGREL1:41;
A4:now assume
      ex x being Element of Y st
            x in EqClass(z,CompF(A,G)) & Pj(a,x)=TRUE;then
      Pj(B_SUP(a,CompF(A,G)),z) = TRUE by BVFUNC_1:def 20;then
      Pj(Ex(a,A,G),z)=TRUE by BVFUNC_2:def 10;
      hence contradiction by A3,MARGREL1:43;
    end;
    for x being Element of Y st
            x in EqClass(z,CompF(A,G)) holds Pj(All(a,B,G),x)<>TRUE
    proof
      let x be Element of Y;
      assume x in EqClass(z,CompF(A,G));then
      A5:Pj(a,x)<>TRUE by A4;
      x in EqClass(x,CompF(B,G)) & EqClass(x,CompF(B,G)) in CompF(B,G)
        by T_1TOPSP:def 1;then
      Pj(B_INF(a,CompF(B,G)),x) = FALSE by A5,BVFUNC_1:def 19;then
      Pj(All(a,B,G),x)=FALSE by BVFUNC_2:def 9;
      hence thesis by MARGREL1:43;
    end; then
    Pj(B_SUP(All(a,B,G),CompF(A,G)),z) = FALSE by BVFUNC_1:def 20;then
    Pj(Ex(All(a,B,G),A,G),z)=FALSE by BVFUNC_2:def 10;then
    'not' Pj(Ex(All(a,B,G),A,G),z)=TRUE by MARGREL1:41;
    hence thesis by VALUAT_1:def 5;
 end;
The Mizar article:

Four Variable Predicate Calculus for Boolean Valued Functions. Part II
