The Mizar article:

Predicate Calculus for Boolean Valued Functions. Part I

by
Shunichi Kobayashi, and
Yatsuka Nakamura

Received December 21, 1998

Copyright (c) 1998 Association of Mizar Users

MML identifier: BVFUNC_3
[ MML identifier index ]


environ

 vocabulary PARTIT1, FUNCT_2, MARGREL1, EQREL_1, BVFUNC_1, ZF_LANG, T_1TOPSP,
      BVFUNC_2, BINARITH, FUNCT_1;
 notation XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, FRAENKEL, EQREL_1, BINARITH,
      BVFUNC_1, BVFUNC_2;
 constructors BINARITH, BVFUNC_2, BVFUNC_1;
 clusters VALUAT_1, MARGREL1, FRAENKEL;
 definitions BVFUNC_1;
 theorems T_1TOPSP, MARGREL1, BINARITH, BVFUNC_1, BVFUNC_2, VALUAT_1;

begin :: Chap. 1  Predicate Calculus

reserve Y for non empty set,
        G for Subset of PARTITIONS(Y),
        a,b,c,u for Element of Funcs(Y,BOOLEAN),
        PA for a_partition of Y;

theorem
    (a 'imp' b) '<' (All(a,PA,G) 'imp' Ex(b,PA,G))
proof
    let z be Element of Y;
    assume Pj(a 'imp' b,z)=TRUE;
then A1:('not' Pj(a,z)) 'or' Pj(b,z)=TRUE by BVFUNC_1:def 11;
A2:('not' Pj(a,z))=TRUE or ('not' Pj(a,z))=FALSE by MARGREL1:39;
A3:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    per cases by A1,A2,BINARITH:7;
    suppose 'not' Pj(a,z)=TRUE;
    then Pj(a,z)=FALSE by MARGREL1:41;
    then Pj(a,z)<>TRUE by MARGREL1:43;
    then Pj(B_INF(a,CompF(PA,G)),z) = FALSE by A3,BVFUNC_1:def 19;
    then Pj(All(a,PA,G),z)=FALSE by BVFUNC_2:def 9;
    hence Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
     =('not' FALSE) 'or' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 11
    .=TRUE 'or' Pj(Ex(b,PA,G),z) by MARGREL1:41
    .=TRUE by BINARITH:19;
    suppose Pj(b,z)=TRUE;
    then Pj(B_SUP(b,CompF(PA,G)),z) = TRUE by A3,BVFUNC_1:def 20;
    then Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_2:def 10;
    hence Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
     =('not' Pj(All(a,PA,G),z)) 'or' TRUE by BVFUNC_1:def 11
    .=TRUE by BINARITH:19;
end;

theorem
    (All(a,PA,G) '&' All(b,PA,G)) '<' (a '&' b)
proof
    let z be Element of Y;
    assume A1:Pj(All(a,PA,G) '&' All(b,PA,G),z)=TRUE;
A2:    Pj(All(a,PA,G) '&' All(b,PA,G),z)
     =Pj(All(a,PA,G),z) '&' Pj(All(b,PA,G),z) by VALUAT_1:def 6;
A3:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
A4: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a,x)=TRUE);
      then Pj(B_INF(a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(a,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(a,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,A2,MARGREL1:45;
    end;
      now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b,x)=TRUE);
      then Pj(B_INF(b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(b,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,A2,MARGREL1:45;
    end;
    then A5:Pj(b,z)=TRUE by A3;
    thus Pj(a '&' b,z) =Pj(a,z) '&' Pj(b,z) by VALUAT_1:def 6
    .=TRUE '&' TRUE by A3,A4,A5
    .=TRUE by MARGREL1:45;
end;

theorem
    (a '&' b) '<' (Ex(a,PA,G) '&' Ex(b,PA,G))
proof
A1:Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) by BVFUNC_2:def 10;
    let z be Element of Y;
    assume A2:Pj(a '&' b,z)=TRUE;
      Pj(a '&' b,z)=Pj(a,z) '&' Pj(b,z) by VALUAT_1:def 6;
then A3: Pj(a,z)=TRUE & Pj(b,z)=TRUE by A2,MARGREL1:45;
A4:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    then Pj(B_SUP(b,CompF(PA,G)),z) = TRUE by A3,BVFUNC_1:def 20;
    then A5:Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_2:def 10;
    thus Pj(Ex(a,PA,G) '&' Ex(b,PA,G),z)
     =Pj(Ex(a,PA,G),z) '&' Pj(Ex(b,PA,G),z) by VALUAT_1:def 6
    .=TRUE '&' TRUE by A1,A3,A4,A5,BVFUNC_1:def 20
    .=TRUE by MARGREL1:45;
end;

theorem
    'not' (All(a,PA,G) '&' All(b,PA,G)) = Ex('not' a,PA,G) 'or' Ex('not' b,PA,G
)
proof
A1:All(a,PA,G) = B_INF(a,CompF(PA,G)) by BVFUNC_2:def 9;
A2:All(b,PA,G) = B_INF(b,CompF(PA,G)) by BVFUNC_2:def 9;
A3:'not' (All(a,PA,G) '&' All(b,PA,G)) '<' (Ex('not' a,PA,G) 'or' Ex('not'
b,PA,G))
  proof
    let z be Element of Y;
    assume Pj('not' (All(a,PA,G) '&' All(b,PA,G)),z)=TRUE;
then A4: 'not' Pj((All(a,PA,G) '&' All(b,PA,G)),z)=TRUE by VALUAT_1:def 5;
      Pj(All(a,PA,G) '&' All(b,PA,G),z)
    =Pj(All(a,PA,G),z) '&' Pj(All(b,PA,G),z) by VALUAT_1:def 6;
then A5:Pj(All(a,PA,G),z) '&' Pj(All(b,PA,G),z)=FALSE by A4,MARGREL1:41;
    per cases by A5,MARGREL1:45;
      suppose A6:Pj(All(a,PA,G),z)=FALSE;
        now assume
A7:   for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a,x)=TRUE;
          Pj(All(a,PA,G),z)<>TRUE by A6,MARGREL1:43;
        hence contradiction by A1,A7,BVFUNC_1:def 19;
      end;
      then consider x1 being Element of Y such that
        A8:x1 in EqClass(z,CompF(PA,G)) & Pj(a,x1)<>TRUE;
        Pj(a,x1)=FALSE by A8,MARGREL1:43;
      then 'not' Pj(a,x1)=TRUE by MARGREL1:41;
      then Pj('not' a,x1)=TRUE by VALUAT_1:def 5;
      then Pj(B_SUP('not' a,CompF(PA,G)),z) = TRUE by A8,BVFUNC_1:def 20;
      then Pj(Ex('not' a,PA,G),z) =TRUE by BVFUNC_2:def 10;
      hence Pj(Ex('not' a,PA,G) 'or' Ex('not' b,PA,G),z)
       =TRUE 'or' Pj(Ex('not' b,PA,G),z) by BVFUNC_1:def 7
      .=TRUE by BINARITH:19;
      suppose A9:Pj(All(b,PA,G),z)=FALSE;
        now assume
A10:    for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b,x)=TRUE;
          Pj(All(b,PA,G),z)<>TRUE by A9,MARGREL1:43;
        hence contradiction by A2,A10,BVFUNC_1:def 19;
      end;
      then consider x1 being Element of Y such that
        A11:x1 in EqClass(z,CompF(PA,G)) & Pj(b,x1)<>TRUE;
        Pj(b,x1)=FALSE by A11,MARGREL1:43;
      then 'not' Pj(b,x1)=TRUE by MARGREL1:41;
      then Pj('not' b,x1)=TRUE by VALUAT_1:def 5;
      then Pj(B_SUP('not' b,CompF(PA,G)),z) = TRUE by A11,BVFUNC_1:def 20;
      then Pj(Ex('not' b,PA,G),z) =TRUE by BVFUNC_2:def 10;
      hence Pj(Ex('not' a,PA,G) 'or' Ex('not' b,PA,G),z)
       =Pj(Ex('not' a,PA,G),z) 'or' TRUE by BVFUNC_1:def 7
      .=TRUE by BINARITH:19;
  end;
    Ex('not' a,PA,G) 'or' Ex('not' b,PA,G) '<'
  'not' (All(a,PA,G) '&' All(b,PA,G))
  proof
    let z be Element of Y;
    assume A12: Pj(Ex('not' a,PA,G) 'or' Ex('not' b,PA,G),z)=TRUE;
A13:Pj(Ex('not' a,PA,G) 'or' Ex('not' b,PA,G),z)
     =Pj(Ex('not' a,PA,G),z) 'or' Pj(Ex('not' b,PA,G),z) by BVFUNC_1:def 7;
A14:  Pj(Ex('not' b,PA,G),z)=TRUE or Pj(Ex('not' b,PA,G),z)=FALSE
      by MARGREL1:39;
    per cases by A12,A13,A14,BINARITH:7;
      suppose A15:Pj(Ex('not' a,PA,G),z)=TRUE;
        now assume
          not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj('not' a,x)=TRUE);
        then Pj(B_SUP('not' a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
        then Pj(Ex('not' a,PA,G),z)=FALSE by BVFUNC_2:def 10;
        hence contradiction by A15,MARGREL1:43;
      end;
      then consider x1 being Element of Y such that
        A16:x1 in EqClass(z,CompF(PA,G)) & Pj('not' a,x1)=TRUE;
        'not' Pj(a,x1)=TRUE by A16,VALUAT_1:def 5;
      then Pj(a,x1)=FALSE by MARGREL1:41;
then A17:      Pj(a,x1)<>TRUE by MARGREL1:43;
      thus Pj('not' (All(a,PA,G) '&' All(b,PA,G)),z)
       ='not' Pj((All(a,PA,G) '&' All(b,PA,G)),z) by VALUAT_1:def 5
      .='not' (Pj(All(a,PA,G),z) '&' Pj(All(b,PA,G),z)) by VALUAT_1:def 6
      .='not' (FALSE '&' Pj(All(b,PA,G),z)) by A1,A16,A17,BVFUNC_1:def 19
      .='not' (FALSE) by MARGREL1:45
      .=TRUE by MARGREL1:41;
      suppose A18:Pj(Ex('not' b,PA,G),z)=TRUE;
        now assume
          not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj('not' b,x)=TRUE);
        then Pj(B_SUP('not' b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
        then Pj(Ex('not' b,PA,G),z)=FALSE by BVFUNC_2:def 10;
        hence contradiction by A18,MARGREL1:43;
      end;
      then consider x1 being Element of Y such that
        A19:x1 in EqClass(z,CompF(PA,G)) & Pj('not' b,x1)=TRUE;
        'not' Pj(b,x1)=TRUE by A19,VALUAT_1:def 5;
      then Pj(b,x1)=FALSE by MARGREL1:41;
then A20:      Pj(b,x1)<>TRUE by MARGREL1:43;
      thus Pj('not' (All(a,PA,G) '&' All(b,PA,G)),z)
       ='not' Pj((All(a,PA,G) '&' All(b,PA,G)),z) by VALUAT_1:def 5
      .='not' (Pj(All(a,PA,G),z) '&' Pj(All(b,PA,G),z)) by VALUAT_1:def 6
      .='not' (Pj(All(a,PA,G),z) '&' FALSE) by A2,A19,A20,BVFUNC_1:def 19
      .='not' (FALSE) by MARGREL1:45
      .=TRUE by MARGREL1:41;
  end;
  hence thesis by A3,BVFUNC_1:18;
end;

theorem
    'not' (Ex(a,PA,G) '&' Ex(b,PA,G)) = All('not' a,PA,G) 'or' All('not' b,PA,G
)
proof
A1:All('not' a,PA,G) = B_INF('not' a,CompF(PA,G)) by BVFUNC_2:def 9;
A2:All('not' b,PA,G) = B_INF('not' b,CompF(PA,G)) by BVFUNC_2:def 9;
A3:Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) by BVFUNC_2:def 10;
A4:Ex(b,PA,G) = B_SUP(b,CompF(PA,G)) by BVFUNC_2:def 10;
A5:'not' (Ex(a,PA,G) '&' Ex(b,PA,G)) '<' (All('not' a,PA,G) 'or' All('not'
b,PA,G))
  proof
    let z be Element of Y;
    assume Pj('not' (Ex(a,PA,G) '&' Ex(b,PA,G)),z)=TRUE;
    then 'not' Pj((Ex(a,PA,G) '&' Ex(b,PA,G)),z)=TRUE by VALUAT_1:def 5;
    then Pj((Ex(a,PA,G) '&' Ex(b,PA,G)),z)=FALSE by MARGREL1:41;
then A6:Pj(Ex(a,PA,G),z) '&' Pj(Ex(b,PA,G),z)=FALSE by VALUAT_1:def 6;
    per cases by A6,MARGREL1:45;
      suppose A7:Pj(Ex(a,PA,G),z)=FALSE;
A8:  now assume
A9:   (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE);
          Pj(Ex(a,PA,G),z)<>TRUE by A7,MARGREL1:43;
        hence contradiction by A3,A9,BVFUNC_1:def 20;
      end;
A10:  now let x be Element of Y;
        assume x in EqClass(z,CompF(PA,G));
        then Pj(a,x)<>TRUE by A8;
        then Pj(a,x)=FALSE by MARGREL1:43;
        then 'not' Pj(a,x)=TRUE by MARGREL1:41;
        hence Pj('not' a,x)=TRUE by VALUAT_1:def 5;
      end;
      thus Pj(All('not' a,PA,G) 'or' All('not' b,PA,G),z)
       = Pj(All('not' a,PA,G),z) 'or' Pj(All('not' b,PA,G),z) by BVFUNC_1:def 7
      .= TRUE 'or' Pj(All('not' b,PA,G),z) by A1,A10,BVFUNC_1:def 19
      .= TRUE by BINARITH:19;
      suppose A11:Pj(Ex(b,PA,G),z)=FALSE;
A12:  now assume
A13:    (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
          Pj(Ex(b,PA,G),z)<>TRUE by A11,MARGREL1:43;
        hence contradiction by A4,A13,BVFUNC_1:def 20;
      end;
A14:  now let x be Element of Y;
        assume x in EqClass(z,CompF(PA,G));
        then Pj(b,x)<>TRUE by A12;
        then Pj(b,x)=FALSE by MARGREL1:43;
        then 'not' Pj(b,x)=TRUE by MARGREL1:41;
        hence Pj('not' b,x)=TRUE by VALUAT_1:def 5;
      end;
      thus Pj(All('not' a,PA,G) 'or' All('not' b,PA,G),z)
       = Pj(All('not' a,PA,G),z) 'or' Pj(All('not' b,PA,G),z) by BVFUNC_1:def 7
      .= Pj(All('not' a,PA,G),z) 'or' TRUE by A2,A14,BVFUNC_1:def 19
      .= TRUE by BINARITH:19;
  end;
    All('not' a,PA,G) 'or' All('not' b,PA,G) '<'
  'not' (Ex(a,PA,G) '&' Ex(b,PA,G))
  proof
    let z be Element of Y;
    assume Pj(All('not' a,PA,G) 'or' All('not' b,PA,G),z)=TRUE;
    then A15:Pj(All('not' a,PA,G),z) 'or' Pj(All('not'
b,PA,G),z)=TRUE by BVFUNC_1:def 7;
A16:Pj(All('not' b,PA,G),z)=TRUE or Pj(All('not' b,PA,G),z)=FALSE
      by MARGREL1:39;
    per cases by A15,A16,BINARITH:7;
      suppose A17:Pj(All('not' a,PA,G),z)=TRUE;
A18:  now assume
          not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj('not' a,x)=TRUE);
        then Pj(B_INF('not' a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
        then Pj(All('not' a,PA,G),z)=FALSE by BVFUNC_2:def 9;
        hence contradiction by A17,MARGREL1:43;
      end;
A19: now let x be Element of Y;
        assume x in EqClass(z,CompF(PA,G));
        then Pj('not' a,x)=TRUE by A18;
        then 'not' Pj(a,x)=TRUE by VALUAT_1:def 5;
        then Pj(a,x)=FALSE by MARGREL1:41;
        hence Pj(a,x)<>TRUE by MARGREL1:43;
      end;
      thus Pj('not' (Ex(a,PA,G) '&' Ex(b,PA,G)),z)
       ='not' Pj((Ex(a,PA,G) '&' Ex(b,PA,G)),z) by VALUAT_1:def 5
      .='not' (Pj(Ex(a,PA,G),z) '&' Pj(Ex(b,PA,G),z)) by VALUAT_1:def 6
      .='not' (FALSE '&' Pj(Ex(b,PA,G),z)) by A3,A19,BVFUNC_1:def 20
      .='not' (FALSE) by MARGREL1:45
      .=TRUE by MARGREL1:41;
      suppose A20:Pj(All('not' b,PA,G),z)=TRUE;
A21:now assume
          not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj('not' b,x)=TRUE);
        then Pj(B_INF('not' b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
        then Pj(All('not' b,PA,G),z)=FALSE by BVFUNC_2:def 9;
        hence contradiction by A20,MARGREL1:43;
      end;
A22:  now let x be Element of Y;
        assume x in EqClass(z,CompF(PA,G));
        then Pj('not' b,x)=TRUE by A21;
        then 'not' Pj(b,x)=TRUE by VALUAT_1:def 5;
        then Pj(b,x)=FALSE by MARGREL1:41;
        hence Pj(b,x)<>TRUE by MARGREL1:43;
      end;
      thus Pj('not' (Ex(a,PA,G) '&' Ex(b,PA,G)),z)
       ='not' Pj((Ex(a,PA,G) '&' Ex(b,PA,G)),z) by VALUAT_1:def 5
      .='not' (Pj(Ex(a,PA,G),z) '&' Pj(Ex(b,PA,G),z)) by VALUAT_1:def 6
      .='not' (Pj(Ex(a,PA,G),z) '&' FALSE) by A4,A22,BVFUNC_1:def 20
      .='not' (FALSE) by MARGREL1:45
      .=TRUE by MARGREL1:41;
  end;
  hence thesis by A5,BVFUNC_1:18;
end;

theorem
    (All(a,PA,G) 'or' All(b,PA,G)) '<' (a 'or' b)
proof
    let z be Element of Y;
    assume Pj(All(a,PA,G) 'or' All(b,PA,G),z)=TRUE;
then A1:Pj(All(a,PA,G),z) 'or' Pj(All(b,PA,G),z)=TRUE by BVFUNC_1:def 7;
A2: Pj(All(a,PA,G),z)=TRUE or Pj(All(a,PA,G),z)=FALSE
      by MARGREL1:39;
A3:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    per cases by A1,A2,BINARITH:7;
      suppose A4:Pj(All(a,PA,G),z)=TRUE;
A5:  now assume
          not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a,x)=TRUE);
        then Pj(B_INF(a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
        then Pj(All(a,PA,G),z)=FALSE by BVFUNC_2:def 9;
        hence contradiction by A4,MARGREL1:43;
      end;
      thus Pj(a 'or' b,z) = Pj(a,z) 'or' Pj(b,z) by BVFUNC_1:def 7
      .= TRUE 'or' Pj(b,z) by A3,A5
      .= TRUE by BINARITH:19;
      suppose A6:Pj(All(b,PA,G),z)=TRUE;
A7:  now assume
          not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b,x)=TRUE);
        then Pj(B_INF(b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
        then Pj(All(b,PA,G),z)=FALSE by BVFUNC_2:def 9;
        hence contradiction by A6,MARGREL1:43;
      end;
      thus Pj(a 'or' b,z) = Pj(a,z) 'or' Pj(b,z) by BVFUNC_1:def 7
      .= Pj(a,z) 'or' TRUE by A3,A7
      .= TRUE by BINARITH:19;
end;

theorem
    (a 'or' b) '<' (Ex(a,PA,G) 'or' Ex(b,PA,G))
proof
A1:Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) by BVFUNC_2:def 10;
A2:Ex(b,PA,G) = B_SUP(b,CompF(PA,G)) by BVFUNC_2:def 10;
    let z be Element of Y;
    assume Pj(a 'or' b,z)=TRUE;
then A3:Pj(a,z) 'or' Pj(b,z)=TRUE by BVFUNC_1:def 7;
A4: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
A5:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    per cases by A3,A4,BINARITH:7;
    suppose A6: Pj(a,z)=TRUE;
    thus Pj(Ex(a,PA,G) 'or' Ex(b,PA,G),z)
     =Pj(Ex(a,PA,G),z) 'or' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 7
    .=TRUE 'or' Pj(Ex(b,PA,G),z) by A1,A5,A6,BVFUNC_1:def 20
    .=TRUE by BINARITH:19;
    suppose A7: Pj(b,z)=TRUE;
    thus Pj(Ex(a,PA,G) 'or' Ex(b,PA,G),z)
     =Pj(Ex(a,PA,G),z) 'or' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 7
    .=Pj(Ex(a,PA,G),z) 'or' TRUE by A2,A5,A7,BVFUNC_1:def 20
    .=TRUE by BINARITH:19;
end;

theorem
    (a 'xor' b) '<'
   ('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)) 'or' 'not' (Ex(a,PA,G) 'xor' Ex(
'not' b,PA,G)))
proof
A1:Ex('not' a,PA,G) = B_SUP('not' a,CompF(PA,G)) by BVFUNC_2:def 10;
A2:Ex('not' b,PA,G) = B_SUP('not' b,CompF(PA,G)) by BVFUNC_2:def 10;
    let z be Element of Y;
    assume A3:Pj(a 'xor' b,z)=TRUE;
A4:  Pj(a 'xor' b,z) =Pj(a,z) 'xor' Pj(b,z) by BVFUNC_1:def 8
    .=('not' Pj(a,z) '&' Pj(b,z)) 'or' (Pj(a,z) '&' 'not' Pj(b,z))
       by BINARITH:def 2;
A5:  (Pj(a,z) '&' 'not' Pj(b,z))=TRUE or
    (Pj(a,z) '&' 'not' Pj(b,z))=FALSE by MARGREL1:39;
A6:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    A7:'not' FALSE=TRUE & 'not' TRUE=FALSE by MARGREL1:41;
    A8:FALSE '&' TRUE =FALSE by MARGREL1:49;
    per cases by A3,A4,A5,BINARITH:7;
      suppose ('not' Pj(a,z) '&' Pj(b,z))=TRUE;
      then A9:'not' Pj(a,z)=TRUE & Pj(b,z)=TRUE by MARGREL1:45;
      then Pj('not' a,z)=TRUE by VALUAT_1:def 5;
then A10:      Pj(B_SUP('not' a,CompF(PA,G)),z) = TRUE by A6,BVFUNC_1:def 20;
        Pj(B_SUP(b,CompF(PA,G)),z) = TRUE by A6,A9,BVFUNC_1:def 20;
      then A11:Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_2:def 10;
      A12:Pj(Ex('not' a,PA,G) 'xor' Ex(b,PA,G),z)
       =Pj(Ex('not' a,PA,G),z) 'xor' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 8
      .=FALSE 'or' FALSE by A1,A7,A8,A10,A11,BINARITH:def 2
      .=FALSE by BINARITH:7;
      A13:Pj('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G)),z)
      ='not' Pj((Ex(a,PA,G) 'xor' Ex('not' b,PA,G)),z) by VALUAT_1:def 5;
      thus Pj('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)) 'or'
         'not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G)),z)
      =Pj('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)),z) 'or'
       Pj('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G)),z) by BVFUNC_1:def 7
     .='not' FALSE 'or' 'not' Pj((Ex(a,PA,G) 'xor' Ex('not'
b,PA,G)),z) by A12,A13,VALUAT_1:def 5
     .=TRUE 'or' 'not' Pj((Ex(a,PA,G) 'xor' Ex('not' b,PA,G)),z) by MARGREL1:41
     .=TRUE by BINARITH:19;
      suppose (Pj(a,z) '&' 'not' Pj(b,z))=TRUE;
      then A14:Pj(a,z)=TRUE & 'not' Pj(b,z)=TRUE by MARGREL1:45;
      then Pj('not' b,z)=TRUE by VALUAT_1:def 5;
then A15:  Pj(B_SUP('not' b,CompF(PA,G)),z) = TRUE by A6,BVFUNC_1:def 20;
        Pj(B_SUP(a,CompF(PA,G)),z) = TRUE by A6,A14,BVFUNC_1:def 20;
      then A16:Pj(Ex(a,PA,G),z)=TRUE by BVFUNC_2:def 10;
      A17:Pj(Ex(a,PA,G) 'xor' Ex('not' b,PA,G),z)
       =Pj(Ex(a,PA,G),z) 'xor' Pj(Ex('not' b,PA,G),z) by BVFUNC_1:def 8
      .=FALSE 'or' FALSE by A2,A7,A8,A15,A16,BINARITH:def 2
      .=FALSE by BINARITH:7;
      A18:Pj('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G)),z)
      ='not' Pj((Ex(a,PA,G) 'xor' Ex('not' b,PA,G)),z) by VALUAT_1:def 5;
      thus Pj('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)) 'or'
         'not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G)),z)
      =Pj('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)),z) 'or'
       Pj('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G)),z) by BVFUNC_1:def 7
     .='not' Pj((Ex('not' a,PA,G) 'xor' Ex(b,PA,G)),z) 'or' 'not'
FALSE by A17,A18,VALUAT_1:def 5
     .='not' Pj((Ex('not' a,PA,G) 'xor' Ex(b,PA,G)),z) 'or' TRUE by MARGREL1:41
     .=TRUE by BINARITH:19;
end;

theorem
    All(a 'or' b,PA,G) '<' All(a,PA,G) 'or' Ex(b,PA,G)
proof
    let z be Element of Y;
    assume A1:Pj(All(a 'or' b,PA,G),z)=TRUE;
A2: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'or' b,x)=TRUE);
      then Pj(B_INF(a 'or' b,CompF(PA,G)),z)=FALSE by BVFUNC_1:def 19;
      then Pj(All(a 'or' b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      hence contradiction by A1,MARGREL1:43;
    end;
    per cases;
    suppose (ex x being Element of Y st
        x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
      then Pj(B_SUP(b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 20;
      then Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_2:def 10;
      hence Pj(All(a,PA,G) 'or' Ex(b,PA,G),z)
       =Pj(All(a,PA,G),z) 'or' TRUE by BVFUNC_1:def 7
      .=TRUE by BINARITH:19;
    suppose (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a,x)=TRUE) & not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
      then Pj(B_INF(a,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 19;
      then Pj(All(a,PA,G),z)=TRUE by BVFUNC_2:def 9;
      hence Pj(All(a,PA,G) 'or' Ex(b,PA,G),z)
       =TRUE 'or' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 7
      .=TRUE by BINARITH:19;
    suppose A3:
      not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a,x)=TRUE) &
      not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
      then consider x1 being Element of Y such that
A4:  x1 in EqClass(z,CompF(PA,G)) & Pj(a,x1)<>TRUE;
A5:  Pj(b,x1)<>TRUE by A3,A4;
      A6:Pj(a,x1)=FALSE by A4,MARGREL1:43;
A7:  Pj(a 'or' b,x1)
       = Pj(a,x1) 'or' Pj(b,x1) by BVFUNC_1:def 7
      .= FALSE 'or' FALSE by A5,A6,MARGREL1:43
      .= FALSE by BINARITH:7;
        Pj(a 'or' b,x1)=TRUE by A2,A4;
      hence thesis by A7,MARGREL1:43;
end;

Lm1:now let Y,a,b,G,PA;
 let z be Element of Y;
 assume A1:Pj(All(a 'or' b,PA,G),z)=TRUE;
 assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
  Pj(a 'or' b,x)=TRUE);
 then Pj(B_INF(a 'or' b,CompF(PA,G)),z)=FALSE by BVFUNC_1:def 19;
 then Pj(All(a 'or' b,PA,G),z)=FALSE by BVFUNC_2:def 9;
 hence contradiction by A1,MARGREL1:43;
end;

theorem
    All(a 'or' b,PA,G) '<' Ex(a,PA,G) 'or' All(b,PA,G)
proof
  let z be Element of Y;
  assume A1:Pj(All(a 'or' b,PA,G),z)=TRUE;
  per cases;
  suppose (ex x being Element of Y st
          x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE);
    then Pj(B_SUP(a,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 20;
    then Pj(Ex(a,PA,G),z)=TRUE by BVFUNC_2:def 10;
    hence Pj(Ex(a,PA,G) 'or' All(b,PA,G),z)
     = TRUE 'or' Pj(All(b,PA,G),z) by BVFUNC_1:def 7
    .=TRUE by BINARITH:19;
  suppose (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
       Pj(b,x)=TRUE) &
    not (ex x being Element of Y st
          x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE);
    then Pj(B_INF(b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 19;
    then Pj(All(b,PA,G),z)=TRUE by BVFUNC_2:def 9;
    hence Pj(Ex(a,PA,G) 'or' All(b,PA,G),z)
     =Pj(Ex(a,PA,G),z) 'or' TRUE by BVFUNC_1:def 7
    .=TRUE by BINARITH:19;
  suppose A2:
   not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
       Pj(b,x)=TRUE) & not (ex x being Element of Y st
          x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE);
    then consider x1 being Element of Y such that
      A3: x1 in EqClass(z,CompF(PA,G)) & Pj(b,x1)<>TRUE;
A4:Pj(a,x1)<>TRUE by A2,A3;
A5:Pj(b,x1)=FALSE by A3,MARGREL1:43;
A6:  Pj(a 'or' b,x1)
     = Pj(a,x1) 'or' Pj(b,x1) by BVFUNC_1:def 7
    .= FALSE 'or' FALSE by A4,A5,MARGREL1:43
    .= FALSE by BINARITH:7;
      Pj(a 'or' b,x1)=TRUE by A1,A3,Lm1;
  hence thesis by A6,MARGREL1:43;
end;

theorem
    All(a 'or' b,PA,G) '<' Ex(a,PA,G) 'or' Ex(b,PA,G)
proof
  let z be Element of Y;
  assume A1:Pj(All(a 'or' b,PA,G),z)=TRUE;
A2:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    then Pj(a 'or' b,z)=TRUE by A1,Lm1;
    then A3:Pj(a,z) 'or' Pj(b,z)=TRUE by BVFUNC_1:def 7;
A4:Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
    per cases by A3,A4,BINARITH:7;
    suppose Pj(a,z)=TRUE;
    then Pj(B_SUP(a,CompF(PA,G)),z) = TRUE by A2,BVFUNC_1:def 20;
    then Pj(Ex(a,PA,G),z)=TRUE by BVFUNC_2:def 10;
    hence Pj(Ex(a,PA,G) 'or' Ex(b,PA,G),z)
     =TRUE 'or' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 7
    .=TRUE by BINARITH:19;
    suppose Pj(b,z)=TRUE;
    then Pj(B_SUP(b,CompF(PA,G)),z) = TRUE by A2,BVFUNC_1:def 20;
    then Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_2:def 10;
    hence Pj(Ex(a,PA,G) 'or' Ex(b,PA,G),z)
     =Pj(Ex(a,PA,G),z) 'or' TRUE by BVFUNC_1:def 7
    .=TRUE by BINARITH:19;
end;

theorem
    Ex(a,PA,G) '&' All(b,PA,G) '<' Ex(a '&' b,PA,G)
proof
    let z be Element of Y;
    assume Pj(Ex(a,PA,G) '&' All(b,PA,G),z)=TRUE;
then A1:    Pj(Ex(a,PA,G),z) '&' Pj(All(b,PA,G),z)=TRUE by VALUAT_1:def 6;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE);
      then Pj(B_SUP(a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(a,PA,G),z)=FALSE by BVFUNC_2:def 10;
      then Pj(Ex(a,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
    then consider x1 being Element of Y such that
      A2:x1 in EqClass(z,CompF(PA,G)) & Pj(a,x1)=TRUE;
A3: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b,x)=TRUE);
      then Pj(B_INF(b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(b,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
      Pj(a '&' b,x1)
     =Pj(a,x1) '&' Pj(b,x1) by VALUAT_1:def 6
    .=TRUE '&' TRUE by A2,A3
    .=TRUE by MARGREL1:45;
    then Pj(B_SUP(a '&' b,CompF(PA,G)),z) = TRUE by A2,BVFUNC_1:def 20;
    hence thesis by BVFUNC_2:def 10;
end;

theorem
    All(a,PA,G) '&' Ex(b,PA,G) '<' Ex(a '&' b,PA,G)
proof
    let z be Element of Y;
    assume Pj(All(a,PA,G) '&' Ex(b,PA,G),z)=TRUE;
then A1:    Pj(All(a,PA,G),z) '&' Pj(Ex(b,PA,G),z)=TRUE by VALUAT_1:def 6;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
      then Pj(B_SUP(b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(b,PA,G),z)=FALSE by BVFUNC_2:def 10;
      then Pj(Ex(b,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
    then consider x1 being Element of Y such that
      A2:x1 in EqClass(z,CompF(PA,G)) & Pj(b,x1)=TRUE;
A3: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a,x)=TRUE);
      then Pj(B_INF(a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(a,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(a,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
      Pj(a '&' b,x1)
     =Pj(a,x1) '&' Pj(b,x1) by VALUAT_1:def 6
    .=TRUE '&' TRUE by A2,A3
    .=TRUE by MARGREL1:45;
    then Pj(B_SUP(a '&' b,CompF(PA,G)),z) = TRUE by A2,BVFUNC_1:def 20;
    hence thesis by BVFUNC_2:def 10;
end;

Lm2: now let Y,a,b,G,PA; let z be Element of Y;
    assume A1:Pj(All(a 'imp' b,PA,G),z)=TRUE;
      assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds
         Pj(a 'imp' b,x)=TRUE);
      then Pj(B_INF(a 'imp' b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(a 'imp' b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      hence contradiction by A1,MARGREL1:43;
  end;

theorem
    All(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G)
proof
A1:All(a,PA,G) = B_INF(a,CompF(PA,G)) by BVFUNC_2:def 9;
    let z be Element of Y;
    assume A2:Pj(All(a 'imp' b,PA,G),z)=TRUE;
A3:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    per cases;
    suppose (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
      then Pj(B_SUP(b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 20;
      then Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_2:def 10;
      hence Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
       =('not' Pj(All(a,PA,G),z)) 'or' TRUE by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
    suppose A4: (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a,x)=TRUE) & not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
then A5:  Pj(b,z)<>TRUE by A3;
      A6:Pj(a,z)=TRUE by A3,A4;
A7:      Pj(a 'imp' b,z)
       =('not' Pj(a,z)) 'or' Pj(b,z) by BVFUNC_1:def 11
      .=('not' TRUE) 'or' FALSE by A5,A6,MARGREL1:43
      .=FALSE 'or' FALSE by MARGREL1:41
      .=FALSE by BINARITH:7;
        Pj(a 'imp' b,z)=TRUE by A2,A3,Lm2;
    hence thesis by A7,MARGREL1:43;
    suppose
A8:  not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a,x)=TRUE) & not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
    thus Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
       =('not' Pj(All(a,PA,G),z)) 'or' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 11
      .=('not' FALSE) 'or' Pj(Ex(b,PA,G),z) by A1,A8,BVFUNC_1:def 19
      .=TRUE 'or' Pj(Ex(b,PA,G),z) by MARGREL1:41
      .=TRUE by BINARITH:19;
end;

theorem
    All(a 'imp' b,PA,G) '<' Ex(a,PA,G) 'imp' Ex(b,PA,G)
proof
A1:Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) by BVFUNC_2:def 10;
    let z be Element of Y;
    assume A2:Pj(All(a 'imp' b,PA,G),z)=TRUE;
    per cases;
    suppose (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
      then Pj(B_SUP(b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 20;
      then Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_2:def 10;
      hence Pj(Ex(a,PA,G) 'imp' Ex(b,PA,G),z)
       =('not' Pj(Ex(a,PA,G),z)) 'or' TRUE by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
    suppose A3: (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE) &
      not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
      then consider x1 being Element of Y such that
        A4:x1 in EqClass(z,CompF(PA,G)) & Pj(a,x1)=TRUE;
A5:      Pj(b,x1)<>TRUE by A3,A4;
A6:      Pj(a 'imp' b,x1)
       =('not' Pj(a,x1)) 'or' Pj(b,x1) by BVFUNC_1:def 11
      .=('not' TRUE) 'or' FALSE by A4,A5,MARGREL1:43
      .=FALSE 'or' FALSE by MARGREL1:41
      .=FALSE by BINARITH:7;
        Pj(a 'imp' b,x1)=TRUE by A2,A4,Lm2;
    hence thesis by A6,MARGREL1:43;
    suppose
A7:  not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE) &
      not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
      thus Pj(Ex(a,PA,G) 'imp' Ex(b,PA,G),z)
       =('not' Pj(Ex(a,PA,G),z)) 'or' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 11
      .=('not' FALSE) 'or' Pj(Ex(b,PA,G),z) by A1,A7,BVFUNC_1:def 20
      .=TRUE 'or' Pj(Ex(b,PA,G),z) by MARGREL1:41
      .=TRUE by BINARITH:19;
end;

theorem
    Ex(a,PA,G) 'imp' All(b,PA,G) '<' All(a 'imp' b,PA,G)
proof
    let z be Element of Y;
    assume Pj(Ex(a,PA,G) 'imp' All(b,PA,G),z)=TRUE;
    then A1:('not' Pj(Ex(a,PA,G),z)) 'or' Pj(All(b,PA,G),z)=TRUE by BVFUNC_1:
def 11;
    per cases;
    suppose A2:
      (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b,x)=TRUE);
        for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'imp' b,x)=TRUE
      proof
        let x be Element of Y;
        assume A3: x in EqClass(z,CompF(PA,G));
        thus Pj(a 'imp' b,x)=('not' Pj(a,x)) 'or' Pj(b,x) by BVFUNC_1:def 11
        .=('not' Pj(a,x)) 'or' TRUE by A2,A3
        .=TRUE by BINARITH:19;
      end;
      then Pj(B_INF(a 'imp' b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 19;
    hence thesis by BVFUNC_2:def 9;
    suppose A4: (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE) &
      not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b,x)=TRUE);
      then Pj(B_SUP(a,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 20;
      then Pj(Ex(a,PA,G),z)=TRUE by BVFUNC_2:def 10;
then A5:      'not' Pj(Ex(a,PA,G),z)=FALSE by MARGREL1:41;
        Pj(B_INF(b,CompF(PA,G)),z) = FALSE by A4,BVFUNC_1:def 19;
      then Pj(All(b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(b,PA,G),z)<>TRUE by MARGREL1:43;
    hence thesis by A1,A5,BINARITH:7;
    suppose
A6:   not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE) &
      not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b,x)=TRUE);
        now let x be Element of Y;
        assume x in EqClass(z,CompF(PA,G));
then A7:    Pj(a,x)<>TRUE by A6;
        thus Pj(a 'imp' b,x) =('not' Pj(a,x)) 'or' Pj(b,x) by BVFUNC_1:def 11
        .=('not' FALSE) 'or' Pj(b,x) by A7,MARGREL1:43
        .=TRUE 'or' Pj(b,x) by MARGREL1:41
        .=TRUE by BINARITH:19;
      end;
      then Pj(B_INF(a 'imp' b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 19;
    hence thesis by BVFUNC_2:def 9;
end;

theorem
    (a 'imp' b) '<' (a 'imp' Ex(b,PA,G))
proof
    let z be Element of Y;
    assume Pj(a 'imp' b,z)=TRUE;
    then A1:('not' Pj(a,z)) 'or' Pj(b,z)=TRUE by BVFUNC_1:def 11;
A2: ('not' Pj(a,z))=TRUE or ('not' Pj(a,z))=FALSE by MARGREL1:39;
A3:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    per cases by A1,A2,BINARITH:7;
    suppose 'not' Pj(a,z)=TRUE;
    hence Pj(a 'imp' Ex(b,PA,G),z)
     =TRUE 'or' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 11
    .=TRUE by BINARITH:19;
    suppose Pj(b,z)=TRUE;
    then Pj(B_SUP(b,CompF(PA,G)),z) = TRUE by A3,BVFUNC_1:def 20;
    then Pj(Ex(b,PA,G),z) =TRUE by BVFUNC_2:def 10;
    hence Pj(a 'imp' Ex(b,PA,G),z)
     =('not' Pj(a,z)) 'or' TRUE by BVFUNC_1:def 11
    .=TRUE by BINARITH:19;
end;

theorem
    (a 'imp' b) '<' (All(a,PA,G) 'imp' b)
proof
    let z be Element of Y;
    assume Pj(a 'imp' b,z)=TRUE;
    then A1:('not' Pj(a,z)) 'or' Pj(b,z)=TRUE by BVFUNC_1:def 11;
A2: ('not' Pj(a,z))=TRUE or ('not' Pj(a,z))=FALSE by MARGREL1:39;
A3:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    per cases by A1,A2,BINARITH:7;
    suppose 'not' Pj(a,z)=TRUE;
    then Pj(a,z)=FALSE by MARGREL1:41;
    then Pj(a,z)<>TRUE by MARGREL1:43;
    then Pj(B_INF(a,CompF(PA,G)),z) = FALSE by A3,BVFUNC_1:def 19;
    then Pj(All(a,PA,G),z)=FALSE by BVFUNC_2:def 9;
    hence Pj(All(a,PA,G) 'imp' b,z)
     =('not' FALSE) 'or' Pj(b,z) by BVFUNC_1:def 11
    .=TRUE 'or' Pj(b,z) by MARGREL1:41
    .=TRUE by BINARITH:19;
    suppose Pj(b,z)=TRUE;
    hence Pj(All(a,PA,G) 'imp' b,z)
     =('not' Pj(All(a,PA,G),z)) 'or' TRUE by BVFUNC_1:def 11
    .=TRUE by BINARITH:19;
end;

theorem
    Ex(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G)
proof
    let z be Element of Y;
    assume A1:Pj(Ex(a 'imp' b,PA,G),z)=TRUE;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a 'imp' b,x)=TRUE);
      then Pj(B_SUP(a 'imp' b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(a 'imp' b,PA,G),z)=FALSE by BVFUNC_2:def 10;
      hence contradiction by A1,MARGREL1:43;
    end;
    then consider x1 being Element of Y such that
      A2:x1 in EqClass(z,CompF(PA,G)) & Pj(a 'imp' b,x1)=TRUE;
    A3:('not' Pj(a,x1)) 'or' Pj(b,x1)=TRUE by A2,BVFUNC_1:def 11;
A4:    Pj(b,x1)=TRUE or Pj(b,x1)=FALSE by MARGREL1:39;
    per cases by A3,A4,BINARITH:7;
      suppose ('not' Pj(a,x1))=TRUE;
      then Pj(a,x1)=FALSE by MARGREL1:41;
      then Pj(a,x1)<>TRUE by MARGREL1:43;
      then Pj(B_INF(a,CompF(PA,G)),z) = FALSE by A2,BVFUNC_1:def 19;
      then Pj(All(a,PA,G),z)=FALSE by BVFUNC_2:def 9;
      hence Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
       =('not' FALSE) 'or' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 11
      .=TRUE 'or' Pj(Ex(b,PA,G),z) by MARGREL1:41
      .=TRUE by BINARITH:19;
      suppose Pj(b,x1)=TRUE;
      then Pj(B_SUP(b,CompF(PA,G)),z) = TRUE by A2,BVFUNC_1:def 20;
      then Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_2:def 10;
      hence Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
       =('not' Pj(All(a,PA,G),z)) 'or' TRUE by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
end;

theorem
    All(a,PA,G) '<' Ex(b,PA,G) 'imp' Ex(a '&' b,PA,G)
proof
    let z be Element of Y;
    assume A1:Pj(All(a,PA,G),z)=TRUE;
A2:now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a,x)=TRUE);
      then Pj(B_INF(a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(a,PA,G),z)=FALSE by BVFUNC_2:def 9;
      hence contradiction by A1,MARGREL1:43;
    end;
    per cases;
    suppose A3:Pj(Ex(b,PA,G),z)=TRUE;
        now assume
          not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
        then Pj(B_SUP(b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
        then Pj(Ex(b,PA,G),z)=FALSE by BVFUNC_2:def 10;
        hence contradiction by A3,MARGREL1:43;
      end;
      then consider x1 being Element of Y such that
        A4:x1 in EqClass(z,CompF(PA,G)) & Pj(b,x1)=TRUE;
        Pj(a '&' b,x1)
       =Pj(a,x1) '&' Pj(b,x1) by VALUAT_1:def 6
      .=TRUE '&' TRUE by A2,A4
      .=TRUE by MARGREL1:45;
      then Pj(B_SUP(a '&' b,CompF(PA,G)),z) = TRUE by A4,BVFUNC_1:def 20;
      then Pj(Ex(a '&' b,PA,G),z)=TRUE by BVFUNC_2:def 10;
      hence Pj(Ex(b,PA,G) 'imp' Ex(a '&' b,PA,G),z)
       =('not' Pj(Ex(b,PA,G),z)) 'or' TRUE by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
    suppose Pj(Ex(b,PA,G),z)<>TRUE;
    then Pj(Ex(b,PA,G),z)=FALSE by MARGREL1:43;
    hence Pj(Ex(b,PA,G) 'imp' Ex(a '&' b,PA,G),z)
     =('not' FALSE) 'or' Pj(Ex(a '&' b,PA,G),z) by BVFUNC_1:def 11
    .=TRUE 'or' Pj(Ex(a '&' b,PA,G),z) by MARGREL1:41
    .=TRUE by BINARITH:19;
end;

theorem
    u is_independent_of PA,G implies
   Ex(u 'imp' a,PA,G) '<' (u 'imp' Ex(a,PA,G))
proof
  assume u is_independent_of PA,G;
then A1:u is_dependent_of CompF(PA,G) by BVFUNC_2:def 8;
    let z be Element of Y;
    assume A2:Pj(Ex(u 'imp' a,PA,G),z)=TRUE;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(u 'imp' a,x)=TRUE);
      then Pj(B_SUP(u 'imp' a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(u 'imp' a,PA,G),z)=FALSE by BVFUNC_2:def 10;
      hence contradiction by A2,MARGREL1:43;
    end;
    then consider x1 being Element of Y such that
A3: x1 in EqClass(z,CompF(PA,G)) & Pj(u 'imp' a,x1)=TRUE;
    A4:('not' Pj(u,x1)) 'or' Pj(a,x1)=TRUE by A3,BVFUNC_1:def 11;
A5: ('not' Pj(u,x1))=TRUE or ('not' Pj(u,x1))=FALSE by MARGREL1:39;
A6:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    per cases by A4,A5,BINARITH:7;
    suppose A7:('not' Pj(u,x1))=TRUE;
 u.x1 = u.z by A1,A3,A6,BVFUNC_1:def 18;
    then Pj(u,z)=FALSE by A7,MARGREL1:41;
    hence Pj(u 'imp' Ex(a,PA,G),z)
     =('not' FALSE) 'or' Pj(Ex(a,PA,G),z) by BVFUNC_1:def 11
    .=TRUE 'or' Pj(Ex(a,PA,G),z) by MARGREL1:41
    .=TRUE by BINARITH:19;
    suppose Pj(a,x1)=TRUE;
    then Pj(B_SUP(a,CompF(PA,G)),z) = TRUE by A3,BVFUNC_1:def 20;
    then Pj(Ex(a,PA,G),z)=TRUE by BVFUNC_2:def 10;
    hence Pj(u 'imp' Ex(a,PA,G),z)
     =('not' Pj(u,z)) 'or' TRUE by BVFUNC_1:def 11
    .=TRUE by BINARITH:19;
end;

theorem
    u is_independent_of PA,G implies
   Ex(a 'imp' u,PA,G) '<' (All(a,PA,G) 'imp' u)
proof
  assume u is_independent_of PA,G;
then A1: u is_dependent_of CompF(PA,G) by BVFUNC_2:def 8;
    let z be Element of Y;
    assume A2:Pj(Ex(a 'imp' u,PA,G),z)=TRUE;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a 'imp' u,x)=TRUE);
      then Pj(B_SUP(a 'imp' u,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(a 'imp' u,PA,G),z)=FALSE by BVFUNC_2:def 10;
      hence contradiction by A2,MARGREL1:43;
    end;
    then consider x1 being Element of Y such that
      A3:x1 in EqClass(z,CompF(PA,G)) & Pj(a 'imp' u,x1)=TRUE;
    A4:('not' Pj(a,x1)) 'or' Pj(u,x1)=TRUE by A3,BVFUNC_1:def 11;
A5: ('not' Pj(a,x1))=TRUE or ('not' Pj(a,x1))=FALSE by MARGREL1:39;
A6:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    per cases by A4,A5,BINARITH:7;
    suppose ('not' Pj(a,x1))=TRUE;
    then Pj(a,x1)=FALSE by MARGREL1:41;
    then Pj(a,x1)<>TRUE by MARGREL1:43;
    then Pj(B_INF(a,CompF(PA,G)),z) = FALSE by A3,BVFUNC_1:def 19;
    then Pj(All(a,PA,G),z)=FALSE by BVFUNC_2:def 9;
    hence Pj(All(a,PA,G) 'imp' u,z)
     =('not' FALSE) 'or' Pj(u,z) by BVFUNC_1:def 11
    .=TRUE 'or' Pj(u,z) by MARGREL1:41
    .=TRUE by BINARITH:19;
    suppose A7:Pj(u,x1)=TRUE;
 u.x1 = u.z by A1,A3,A6,BVFUNC_1:def 18;
    hence Pj(All(a,PA,G) 'imp' u,z)
     =('not' Pj(All(a,PA,G),z)) 'or' TRUE by A7,BVFUNC_1:def 11
    .=TRUE by BINARITH:19;
end;

theorem
    All(a,PA,G) 'imp' Ex(b,PA,G) = Ex(a 'imp' b,PA,G)
proof
A1:All(a,PA,G) = B_INF(a,CompF(PA,G)) by BVFUNC_2:def 9;
A2:All(a,PA,G) 'imp' Ex(b,PA,G) '<' Ex(a 'imp' b,PA,G)
  proof
    let z be Element of Y;
    assume Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)=TRUE;
    then A3:('not' Pj(All(a,PA,G),z)) 'or' Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_1:
def 11;
A4: ('not' Pj(All(a,PA,G),z))=TRUE or
    ('not' Pj(All(a,PA,G),z))=FALSE by MARGREL1:39;
    per cases by A3,A4,BINARITH:7;
      suppose ('not' Pj(All(a,PA,G),z))=TRUE;
      then Pj(All(a,PA,G),z)=FALSE by MARGREL1:41;
      then Pj(All(a,PA,G),z)<>TRUE by MARGREL1:43;
      then consider x1 being Element of Y such that
        A5: x1 in EqClass(z,CompF(PA,G)) & Pj(a,x1)<>TRUE
        by A1,BVFUNC_1:def 19;
        Pj(a 'imp' b,x1)
       =('not' Pj(a,x1)) 'or' Pj(b,x1) by BVFUNC_1:def 11
      .=('not' FALSE) 'or' Pj(b,x1) by A5,MARGREL1:43
      .=TRUE 'or' Pj(b,x1) by MARGREL1:41
      .=TRUE by BINARITH:19;
      then Pj(B_SUP(a 'imp' b,CompF(PA,G)),z) = TRUE by A5,BVFUNC_1:def 20;
      hence thesis by BVFUNC_2:def 10;
      suppose A6:Pj(Ex(b,PA,G),z)=TRUE;
        now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
        then Pj(B_SUP(b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
        then Pj(Ex(b,PA,G),z)=FALSE by BVFUNC_2:def 10;
        hence contradiction by A6,MARGREL1:43;
      end;
      then consider x1 being Element of Y such that
A7:  x1 in EqClass(z,CompF(PA,G)) & Pj(b,x1)=TRUE;
        Pj(a 'imp' b,x1) =('not' Pj(a,x1)) 'or' TRUE by A7,BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      then Pj(B_SUP(a 'imp' b,CompF(PA,G)),z) = TRUE by A7,BVFUNC_1:def 20;
      hence thesis by BVFUNC_2:def 10;
  end;
    Ex(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G)
  proof
    let z be Element of Y;
    assume A8:Pj(Ex(a 'imp' b,PA,G),z)=TRUE;
      now assume
        not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a 'imp' b,x)=TRUE);
      then Pj(B_SUP(a 'imp' b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(a 'imp' b,PA,G),z)=FALSE by BVFUNC_2:def 10;
      hence contradiction by A8,MARGREL1:43;
    end;
    then consider x1 being Element of Y such that
      A9:x1 in EqClass(z,CompF(PA,G)) & Pj(a 'imp' b,x1)=TRUE;
    A10:('not' Pj(a,x1)) 'or' Pj(b,x1)=TRUE by A9,BVFUNC_1:def 11;
A11:('not' Pj(a,x1))=TRUE or ('not' Pj(a,x1))=FALSE by MARGREL1:39;
    per cases by A10,A11,BINARITH:7;
    suppose ('not' Pj(a,x1))=TRUE;
    then Pj(a,x1)=FALSE by MARGREL1:41;
    then Pj(a,x1)<>TRUE by MARGREL1:43;
    then Pj(B_INF(a,CompF(PA,G)),z) = FALSE by A9,BVFUNC_1:def 19;
    hence Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
     =('not' FALSE) 'or' Pj(Ex(b,PA,G),z) by A1,BVFUNC_1:def 11
    .=TRUE 'or' Pj(Ex(b,PA,G),z) by MARGREL1:41
    .=TRUE by BINARITH:19;
    suppose Pj(b,x1)=TRUE;
    then Pj(B_SUP(b,CompF(PA,G)),z) = TRUE by A9,BVFUNC_1:def 20;
    then Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_2:def 10;
    hence Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
     =('not' Pj(All(a,PA,G),z)) 'or' TRUE by BVFUNC_1:def 11
    .=TRUE by BINARITH:19;
  end;
  hence thesis by A2,BVFUNC_1:18;
end;

theorem
    All(a,PA,G) 'imp' All(b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G)
proof
    let z be Element of Y;
    assume Pj(All(a,PA,G) 'imp' All(b,PA,G),z)=TRUE;
    then A1:('not'
 Pj(All(a,PA,G),z)) 'or' Pj(All(b,PA,G),z)=TRUE by BVFUNC_1:def 11;
A2:    ('not' Pj(All(a,PA,G),z))=TRUE or
    ('not' Pj(All(a,PA,G),z))=FALSE by MARGREL1:39;
A3:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    per cases by A1,A2,BINARITH:7;
    suppose 'not' Pj(All(a,PA,G),z)=TRUE;
    hence Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
     =TRUE 'or' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 11
    .=TRUE by BINARITH:19;
    suppose A4:Pj(All(b,PA,G),z)=TRUE;
      now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
        Pj(b,x)=TRUE);
      then Pj(B_INF(b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      hence contradiction by A4,MARGREL1:43;
    end;
    then Pj(b,z)=TRUE by A3;
    then Pj(B_SUP(b,CompF(PA,G)),z) = TRUE by A3,BVFUNC_1:def 20;
    then Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_2:def 10;
    hence Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
     =('not' Pj(All(a,PA,G),z)) 'or' TRUE by BVFUNC_1:def 11
    .=TRUE by BINARITH:19;
end;

theorem
    Ex(a,PA,G) 'imp' Ex(b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G)
proof
A1:Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) by BVFUNC_2:def 10;
    let z be Element of Y;
    assume Pj(Ex(a,PA,G) 'imp' Ex(b,PA,G),z)=TRUE;
then A2: ('not' Pj(Ex(a,PA,G),z)) 'or' Pj(Ex(b,PA,G),z)=TRUE by BVFUNC_1:def 11
;
A3:    ('not' Pj(Ex(a,PA,G),z))=TRUE or
    ('not' Pj(Ex(a,PA,G),z))=FALSE by MARGREL1:39;
A4:z in EqClass(z,CompF(PA,G)) &
      EqClass(z,CompF(PA,G)) in CompF(PA,G) by T_1TOPSP:def 1;
    per cases by A2,A3,BINARITH:7;
    suppose ('not' Pj(Ex(a,PA,G),z))=TRUE;
    then Pj(Ex(a,PA,G),z)=FALSE by MARGREL1:41;
    then Pj(Ex(a,PA,G),z)<>TRUE by MARGREL1:43;
    then Pj(a,z)<>TRUE by A1,A4,BVFUNC_1:def 20;
    then Pj(B_INF(a,CompF(PA,G)),z) = FALSE by A4,BVFUNC_1:def 19;
    then Pj(All(a,PA,G),z)=FALSE by BVFUNC_2:def 9;
    hence Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
     =('not' FALSE) 'or' Pj(Ex(b,PA,G),z) by BVFUNC_1:def 11
    .=TRUE 'or' Pj(Ex(b,PA,G),z) by MARGREL1:41
    .=TRUE by BINARITH:19;
    suppose Pj(Ex(b,PA,G),z)=TRUE;
    hence Pj(All(a,PA,G) 'imp' Ex(b,PA,G),z)
     =('not' Pj(All(a,PA,G),z)) 'or' TRUE by BVFUNC_1:def 11
    .=TRUE by BINARITH:19;
end;

theorem Th26:
  All(a 'imp' b,PA,G) = All('not' a 'or' b,PA,G)
proof
A1:All(a 'imp' b,PA,G) '<' All('not' a 'or' b,PA,G)
  proof
    let z be Element of Y;
    assume A2:Pj(All(a 'imp' b,PA,G),z)=TRUE;
A3: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'imp' b,x)=TRUE);
      then Pj(B_INF(a 'imp' b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(a 'imp' b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      hence contradiction by A2,MARGREL1:43;
    end;
      now let x be Element of Y;
      assume x in EqClass(z,CompF(PA,G));
      then Pj(a 'imp' b,x)=TRUE by A3;
      then A4:('not' Pj(a,x)) 'or' Pj(b,x)=TRUE by BVFUNC_1:def 11;
A5:   ('not' Pj(a,x))=TRUE or ('not' Pj(a,x))=FALSE by MARGREL1:39;
      per cases by A4,A5,BINARITH:7;
      suppose ('not' Pj(a,x))=TRUE;
      then Pj('not' a,x)=TRUE by VALUAT_1:def 5;
      hence Pj('not' a 'or' b,x)
       =TRUE 'or' Pj(b,x) by BVFUNC_1:def 7
      .=TRUE by BINARITH:19;
      suppose Pj(b,x)=TRUE;
      hence Pj('not' a 'or' b,x)=Pj('not' a,x) 'or' TRUE by BVFUNC_1:def 7
      .=TRUE by BINARITH:19;
    end;
    then Pj(B_INF('not' a 'or' b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 19;
    hence thesis by BVFUNC_2:def 9;
  end;
    All('not' a 'or' b,PA,G) '<' All(a 'imp' b,PA,G)
  proof
    let z be Element of Y;
    assume A6:Pj(All('not' a 'or' b,PA,G),z)=TRUE;
A7:now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj('not' a 'or' b,x)=TRUE);
      then Pj(B_INF('not' a 'or' b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All('not' a 'or' b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      hence contradiction by A6,MARGREL1:43;
    end;
      for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'imp' b,x)=TRUE
    proof
      let x be Element of Y;
      assume x in EqClass(z,CompF(PA,G));
      then Pj('not' a 'or' b,x)=TRUE by A7;
then A8:  Pj('not' a,x) 'or' Pj(b,x)=TRUE by BVFUNC_1:def 7;
A9:  Pj('not' a,x)=TRUE or Pj('not' a,x)=FALSE by MARGREL1:39;
      per cases by A8,A9,BINARITH:7;
      suppose Pj('not' a,x)=TRUE;
      then 'not' Pj(a,x)=TRUE by VALUAT_1:def 5;
      hence Pj(a 'imp' b,x) = TRUE 'or' Pj(b,x) by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      suppose Pj(b,x)=TRUE;
      hence Pj(a 'imp' b,x) =('not' Pj(a,x)) 'or' TRUE by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
    end;
    then Pj(B_INF(a 'imp' b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 19;
    hence thesis by BVFUNC_2:def 9;
  end;
  hence thesis by A1,BVFUNC_1:18;
end;

theorem
     All(a 'imp' b,PA,G) = 'not' (Ex(a '&' 'not' b,PA,G))
proof
    'not' All('not' a 'or' b,PA,G) = Ex('not' ('not'
a 'or' b),PA,G) by BVFUNC_2:20;
then A1:All('not' a 'or' b,PA,G) ='not' Ex('not' ('not' a 'or' b),PA,G)
  by BVFUNC_1:4;
    'not' ('not' a 'or' b)=('not' 'not' a) '&' ('not' b) by BVFUNC_1:16;
  then 'not' ('not' a 'or' b)=a '&' 'not' b by BVFUNC_1:4;
  hence thesis by A1,Th26;
end;

theorem
    Ex(a,PA,G) '<' 'not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G))
proof
    let z be Element of Y;
    assume A1:Pj(Ex(a,PA,G),z)=TRUE;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE);
      then Pj(B_SUP(a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(a,PA,G),z)=FALSE by BVFUNC_2:def 10;
      hence contradiction by A1,MARGREL1:43;
    end;
    then consider x1 being Element of Y such that
      A2:x1 in EqClass(z,CompF(PA,G)) & Pj(a,x1)=TRUE;
A3:Pj('not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G)),z)
     ='not' Pj((All(a 'imp' b,PA,G) '&' All(a 'imp' 'not'
b,PA,G)),z) by VALUAT_1:def 5
    .='not' (Pj(All(a 'imp' b,PA,G),z) '&' Pj(All(a 'imp' 'not' b,PA,G),z))
        by VALUAT_1:def 6;
A4:Pj(a 'imp' b,x1)
     ='not' TRUE 'or' Pj(b,x1) by A2,BVFUNC_1:def 11
    .=FALSE 'or' Pj(b,x1) by MARGREL1:41
    .=Pj(b,x1) by BINARITH:7;
A5:    Pj(a 'imp' 'not' b,x1)
     ='not' TRUE 'or' Pj('not' b,x1) by A2,BVFUNC_1:def 11
    .=FALSE 'or' Pj('not' b,x1) by MARGREL1:41
    .=Pj('not' b,x1) by BINARITH:7;
    per cases by MARGREL1:39;
    suppose Pj(b,x1)=TRUE;
    then Pj(a 'imp' 'not' b,x1)
     ='not' TRUE by A5,VALUAT_1:def 5
    .=FALSE by MARGREL1:41;
    then Pj(a 'imp' 'not' b,x1)<>TRUE by MARGREL1:43;
    then Pj(B_INF(a 'imp' 'not' b,CompF(PA,G)),z) = FALSE by A2,BVFUNC_1:def 19
;
    hence Pj('not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G)),z)
     ='not' (Pj(All(a 'imp' b,PA,G),z) '&' FALSE) by A3,BVFUNC_2:def 9
    .='not' (FALSE) by MARGREL1:45
    .=TRUE by MARGREL1:41;
    suppose Pj(b,x1)=FALSE;
    then Pj(a 'imp' b,x1)<>TRUE by A4,MARGREL1:43;
    then Pj(B_INF(a 'imp' b,CompF(PA,G)),z) = FALSE by A2,BVFUNC_1:def 19;
    hence Pj('not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G)),z)
     ='not' (FALSE '&' Pj(All(a 'imp' 'not' b,PA,G),z)) by A3,BVFUNC_2:def 9
    .='not' (FALSE) by MARGREL1:45
    .=TRUE by MARGREL1:41;
end;

theorem
    Ex(a,PA,G) '<'
    'not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G))
proof
    let z be Element of Y;
    assume A1:Pj(Ex(a,PA,G),z)=TRUE;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE);
      then Pj(B_SUP(a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(a,PA,G),z)=FALSE by BVFUNC_2:def 10;
      hence contradiction by A1,MARGREL1:43;
    end;
    then consider x1 being Element of Y such that
      A2:x1 in EqClass(z,CompF(PA,G)) & Pj(a,x1)=TRUE;
A3:Pj(a '&' b,x1) =TRUE '&' Pj(b,x1) by A2,VALUAT_1:def 6
    .=Pj(b,x1) by MARGREL1:50;
A4:Pj(a '&' 'not' b,x1) =TRUE '&' Pj('not' b,x1) by A2,VALUAT_1:def 6
    .=Pj('not' b,x1) by MARGREL1:50;
    A5:Pj('not' Ex(a '&' 'not' b,PA,G),z)='not' Pj(Ex(a '&' 'not'
b,PA,G),z) by VALUAT_1:def 5;
A6:Pj('not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G)),z)
     ='not' Pj(('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not'
b,PA,G)),z) by VALUAT_1:def 5
    .='not' (Pj('not' Ex(a '&' b,PA,G),z) '&'
    Pj('not' Ex(a '&' 'not' b,PA,G),z))
      by VALUAT_1:def 6
    .='not' ('not' Pj(Ex(a '&' b,PA,G),z) '&' 'not' Pj(Ex(a '&' 'not'
b,PA,G),z)) by A5,VALUAT_1:def 5;
    per cases by MARGREL1:39;
    suppose Pj(b,x1)=TRUE;
    then Pj(B_SUP(a '&' b,CompF(PA,G)),z) = TRUE by A2,A3,BVFUNC_1:def 20;
    hence Pj('not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G)),z
)
     ='not' ('not' TRUE '&' 'not' Pj(Ex(a '&' 'not'
b,PA,G),z)) by A6,BVFUNC_2:def 10
    .='not' (FALSE '&' 'not' Pj(Ex(a '&' 'not' b,PA,G),z)) by MARGREL1:41
    .='not' (FALSE) by MARGREL1:45
    .=TRUE by MARGREL1:41;
    suppose Pj(b,x1)=FALSE;
    then Pj(a '&' 'not' b,x1)='not' FALSE by A4,VALUAT_1:def 5;
    then Pj(a '&' 'not' b,x1)=TRUE by MARGREL1:41;
    then Pj(B_SUP(a '&' 'not' b,CompF(PA,G)),z) = TRUE by A2,BVFUNC_1:def 20;
    hence Pj('not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G)),z
)
     ='not' ('not' Pj(Ex(a '&' b,PA,G),z) '&' 'not' TRUE) by A6,BVFUNC_2:def 10
    .='not' ('not' Pj(Ex(a '&' b,PA,G),z) '&' FALSE) by MARGREL1:41
    .='not' (FALSE) by MARGREL1:45
    .=TRUE by MARGREL1:41;
end;

theorem
    Ex(a,PA,G) '&' All(a 'imp' b,PA,G) '<' Ex(a '&' b,PA,G)
proof
    let z be Element of Y;
    assume Pj(Ex(a,PA,G) '&' All(a 'imp' b,PA,G),z)=TRUE;
then A1: Pj(Ex(a,PA,G),z) '&' Pj(All(a 'imp' b,PA,G),z)=TRUE by VALUAT_1:def 6;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE);
      then Pj(B_SUP(a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(a,PA,G),z)=FALSE by BVFUNC_2:def 10;
      then Pj(Ex(a,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
    then consider x1 being Element of Y such that
      A2:x1 in EqClass(z,CompF(PA,G)) & Pj(a,x1)=TRUE;
      now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'imp' b,x)=TRUE);
      then Pj(B_INF(a 'imp' b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(a 'imp' b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(a 'imp' b,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
    then Pj(a 'imp' b,x1)=TRUE by A2;
    then A3:('not' Pj(a,x1)) 'or' Pj(b,x1) =TRUE by BVFUNC_1:def 11;
A4:'not' FALSE=TRUE & 'not' TRUE=FALSE by MARGREL1:41;
      Pj(a '&' b,x1)
     =Pj(a,x1) '&' Pj(b,x1) by VALUAT_1:def 6
    .=TRUE '&' TRUE by A2,A3,A4,BINARITH:7
    .=TRUE by MARGREL1:45;
    then Pj(B_SUP(a '&' b,CompF(PA,G)),z) = TRUE by A2,BVFUNC_1:def 20;
    hence thesis by BVFUNC_2:def 10;
end;

theorem
    Ex(a,PA,G) '&' 'not' Ex(a '&' b,PA,G) '<' 'not' All(a 'imp' b,PA,G)
proof
A1:Ex(a '&' b,PA,G) = B_SUP(a '&' b,CompF(PA,G)) by BVFUNC_2:def 10;
    let z be Element of Y;
    assume Pj(Ex(a,PA,G) '&' 'not' Ex(a '&' b,PA,G),z)=TRUE;
then A2: Pj(Ex(a,PA,G),z) '&' Pj('not' Ex(a '&' b,PA,G),z)=TRUE by VALUAT_1:def
6;
then Pj(Ex(a,PA,G),z)=TRUE & Pj('not' Ex(a '&' b,PA,G),z)=TRUE
        by MARGREL1:45;
    then 'not' Pj(Ex(a '&' b,PA,G),z)=TRUE by VALUAT_1:def 5;
    then Pj(Ex(a '&' b,PA,G),z)=FALSE by MARGREL1:41;
then A3:    Pj(Ex(a '&' b,PA,G),z)<>TRUE by MARGREL1:43;
      now assume
        not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a,x)=TRUE);
      then Pj(B_SUP(a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(a,PA,G),z)=FALSE by BVFUNC_2:def 10;
      then Pj(Ex(a,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A2,MARGREL1:45;
    end;
    then consider x1 being Element of Y such that
      A4:x1 in EqClass(z,CompF(PA,G)) & Pj(a,x1)=TRUE;
      Pj(a '&' b,x1)<>TRUE by A1,A3,A4,BVFUNC_1:def 20;
    then Pj(a '&' b,x1)=FALSE by MARGREL1:43;
then A5:Pj(a,x1) '&' Pj(b,x1)=FALSE by VALUAT_1:def 6;
    per cases by A5,MARGREL1:45;
    suppose Pj(a,x1)=FALSE;
    hence thesis by A4,MARGREL1:43;
    suppose Pj(b,x1)=FALSE;
    then Pj(a 'imp' b,x1)
     =('not' TRUE) 'or' FALSE by A4,BVFUNC_1:def 11
    .=FALSE 'or' FALSE by MARGREL1:41
    .=FALSE by BINARITH:7;
    then Pj(a 'imp' b,x1)<>TRUE by MARGREL1:43;
    then Pj(B_INF(a 'imp' b,CompF(PA,G)),z) = FALSE by A4,BVFUNC_1:def 19;
    then Pj(All(a 'imp' b,PA,G),z)=FALSE by BVFUNC_2:def 9;
    hence Pj('not' All(a 'imp' b,PA,G),z)
     ='not' FALSE by VALUAT_1:def 5
    .=TRUE by MARGREL1:41;
end;

theorem
    All(a 'imp' c,PA,G) '&' All(c 'imp' b,PA,G) '<' All(a 'imp' b,PA,G)
proof
    let z be Element of Y;
    assume Pj(All(a 'imp' c,PA,G) '&' All(c 'imp' b,PA,G),z)=TRUE;
then A1:    Pj(All(a 'imp' c,PA,G),z) '&' Pj(All(c 'imp' b,PA,G),z)=TRUE
       by VALUAT_1:def 6;
A2: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'imp' c,x)=TRUE);
      then Pj(B_INF(a 'imp' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(a 'imp' c,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(a 'imp' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
A3: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(c 'imp' b,x)=TRUE);
      then Pj(B_INF(c 'imp' b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(c 'imp' b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(c 'imp' b,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
      for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'imp' b,x)=TRUE
    proof
      let x be Element of Y;
      assume A4:x in EqClass(z,CompF(PA,G));
      then Pj(a 'imp' c,x)=TRUE by A2;
      then A5:('not' Pj(a,x)) 'or' Pj(c,x)=TRUE by BVFUNC_1:def 11;
A6:  ('not' Pj(a,x))=TRUE or ('not' Pj(a,x))=FALSE by MARGREL1:39;
        Pj(c 'imp' b,x)=TRUE by A3,A4;
      then A7:('not' Pj(c,x)) 'or' Pj(b,x)=TRUE by BVFUNC_1:def 11;
A8:  ('not' Pj(c,x))=TRUE or ('not' Pj(c,x))=FALSE by MARGREL1:39;
      per cases by A5,A6,A7,A8,BINARITH:7;
      suppose ('not' Pj(a,x))=TRUE & ('not' Pj(c,x))=TRUE;
      hence Pj(a 'imp' b,x) =TRUE 'or' Pj(b,x) by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      suppose ('not' Pj(a,x))=TRUE & Pj(b,x)=TRUE;
      hence Pj(a 'imp' b,x) =TRUE 'or' Pj(b,x) by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      suppose A9:Pj(c,x)=TRUE & ('not' Pj(c,x))=TRUE;
      then Pj(c,x)=FALSE by MARGREL1:41;
      hence thesis by A9,MARGREL1:43;
      suppose Pj(c,x)=TRUE & Pj(b,x)=TRUE;
      hence Pj(a 'imp' b,x) =('not' Pj(a,x)) 'or' TRUE by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
    end;
    then Pj(B_INF(a 'imp' b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 19;
    hence thesis by BVFUNC_2:def 9;
end;

theorem
    All(c 'imp' b,PA,G) '&' Ex(a '&' c,PA,G) '<' Ex(a '&' b,PA,G)
proof
    let z be Element of Y;
    assume Pj(All(c 'imp' b,PA,G) '&' Ex(a '&' c,PA,G),z)=TRUE;
then A1:    Pj(All(c 'imp' b,PA,G),z) '&' Pj(Ex(a '&' c,PA,G),z)=TRUE
       by VALUAT_1:def 6;
A2: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(c 'imp' b,x)=TRUE);
      then Pj(B_INF(c 'imp' b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(c 'imp' b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(c 'imp' b,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a '&' c,x)=TRUE);
      then Pj(B_SUP(a '&' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(a '&' c,PA,G),z)=FALSE by BVFUNC_2:def 10;
      then Pj(Ex(a '&' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
    then consider x1 being Element of Y such that
      A3:x1 in EqClass(z,CompF(PA,G)) & Pj(a '&' c,x1)=TRUE;
      Pj(c 'imp' b,x1)=TRUE by A2,A3;
    then A4:('not' Pj(c,x1)) 'or' Pj(b,x1)=TRUE by BVFUNC_1:def 11;
A5:    ('not' Pj(c,x1))=TRUE or
    ('not' Pj(c,x1))=FALSE by MARGREL1:39;
A6:    Pj(a,x1) '&' Pj(c,x1)=TRUE by A3,VALUAT_1:def 6;
    per cases by A4,A5,A6,BINARITH:7,MARGREL1:45;
    suppose A7:(Pj(a,x1)=TRUE & Pj(c,x1)=TRUE) & ('not' Pj(c,x1))=TRUE;
    then Pj(c,x1)=FALSE by MARGREL1:41;
    hence thesis by A7,MARGREL1:43;
    suppose (Pj(a,x1)=TRUE & Pj(c,x1)=TRUE) & Pj(b,x1)=TRUE;
    then Pj(a '&' b,x1) =TRUE '&' TRUE by VALUAT_1:def 6
    .=TRUE by MARGREL1:45;
    then Pj(B_SUP(a '&' b,CompF(PA,G)),z) = TRUE by A3,BVFUNC_1:def 20;
    hence thesis by BVFUNC_2:def 10;
end;

theorem
    All(b 'imp' 'not' c,PA,G) '&' All(a 'imp' c,PA,G) '<'
    All(a 'imp' 'not' b,PA,G)
proof
    let z be Element of Y;
    assume Pj(All(b 'imp' 'not' c,PA,G) '&' All(a 'imp' c,PA,G),z)=TRUE;
then A1:    Pj(All(b 'imp' 'not' c,PA,G),z) '&' Pj(All(a 'imp' c,PA,G),z)=TRUE
       by VALUAT_1:def 6;
A2: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b 'imp' 'not' c,x)=TRUE);
      then Pj(B_INF(b 'imp' 'not' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19
;
      then Pj(All(b 'imp' 'not' c,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(b 'imp' 'not' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
A3: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'imp' c,x)=TRUE);
      then Pj(B_INF(a 'imp' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(a 'imp' c,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(a 'imp' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
      for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'imp' 'not' b,x)=TRUE
    proof
      let x be Element of Y;
      assume A4:x in EqClass(z,CompF(PA,G));
      then Pj(b 'imp' 'not' c,x)=TRUE by A2;
      then A5:('not' Pj(b,x)) 'or' Pj('not' c,x)=TRUE by BVFUNC_1:def 11;
A6:  ('not' Pj(b,x))=TRUE or ('not' Pj(b,x))=FALSE by MARGREL1:39;
        Pj(a 'imp' c,x)=TRUE by A3,A4;
      then A7:('not' Pj(a,x)) 'or' Pj(c,x)=TRUE by BVFUNC_1:def 11;
A8:  ('not' Pj(a,x))=TRUE or ('not' Pj(a,x))=FALSE by MARGREL1:39;
      per cases by A5,A6,A7,A8,BINARITH:7;
      suppose A9:('not' Pj(b,x))=TRUE & ('not' Pj(a,x))=TRUE;
      then Pj('not' b,x)=TRUE by VALUAT_1:def 5;
      hence Pj(a 'imp' 'not' b,x)
       =TRUE 'or' TRUE by A9,BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      suppose ('not' Pj(b,x))=TRUE & Pj(c,x)=TRUE;
      then Pj('not' b,x)=TRUE by VALUAT_1:def 5;
      hence Pj(a 'imp' 'not' b,x) =('not' Pj(a,x)) 'or' TRUE by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      suppose Pj('not' c,x)=TRUE & ('not' Pj(a,x))=TRUE;
      hence Pj(a 'imp' 'not' b,x) =TRUE 'or' Pj('not' b,x) by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      suppose A10:Pj('not' c,x)=TRUE & Pj(c,x)=TRUE;
      then 'not' Pj(c,x)=TRUE by VALUAT_1:def 5;
      then Pj(c,x)=FALSE by MARGREL1:41;
      hence thesis by A10,MARGREL1:43;
    end;
    then Pj(B_INF(a 'imp' 'not' b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 19;
    hence thesis by BVFUNC_2:def 9;
end;

theorem
    All(b 'imp' c,PA,G) '&' All(a 'imp' 'not' c,PA,G) '<'
    All(a 'imp' 'not' b,PA,G)
proof
    let z be Element of Y;
    assume Pj(All(b 'imp' c,PA,G) '&' All(a 'imp' 'not' c,PA,G),z)=TRUE;
then A1:    Pj(All(b 'imp' c,PA,G),z) '&' Pj(All(a 'imp' 'not' c,PA,G),z)=TRUE
       by VALUAT_1:def 6;
A2: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b 'imp' c,x)=TRUE);
      then Pj(B_INF(b 'imp' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(b 'imp' c,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(b 'imp' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
A3: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'imp' 'not' c,x)=TRUE);
      then Pj(B_INF(a 'imp' 'not' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19
;
      then Pj(All(a 'imp' 'not' c,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(a 'imp' 'not' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
      for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'imp' 'not' b,x)=TRUE
    proof
      let x be Element of Y;
      assume A4:x in EqClass(z,CompF(PA,G));
      then Pj(b 'imp' c,x)=TRUE by A2;
      then A5:('not' Pj(b,x)) 'or' Pj(c,x)=TRUE by BVFUNC_1:def 11;
A6:  ('not' Pj(b,x))=TRUE or ('not' Pj(b,x))=FALSE by MARGREL1:39;
        Pj(a 'imp' 'not' c,x)=TRUE by A3,A4;
      then A7:('not' Pj(a,x)) 'or' Pj('not' c,x)=TRUE by BVFUNC_1:def 11;
A8:  ('not' Pj(a,x))=TRUE or ('not' Pj(a,x))=FALSE by MARGREL1:39;
      per cases by A5,A6,A7,A8,BINARITH:7;
      suppose A9:('not' Pj(b,x))=TRUE & ('not' Pj(a,x))=TRUE;
      then Pj('not' b,x)=TRUE by VALUAT_1:def 5;
      hence Pj(a 'imp' 'not' b,x) =TRUE 'or' TRUE by A9,BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      suppose ('not' Pj(b,x))=TRUE & Pj('not' c,x)=TRUE;
      then Pj('not' b,x)=TRUE by VALUAT_1:def 5;
      hence Pj(a 'imp' 'not' b,x) =('not' Pj(a,x)) 'or' TRUE by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      suppose Pj(c,x)=TRUE & ('not' Pj(a,x))=TRUE;
      hence Pj(a 'imp' 'not' b,x) =TRUE 'or' Pj('not' b,x) by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      suppose A10:Pj(c,x)=TRUE & Pj('not' c,x)=TRUE;
      then 'not' Pj(c,x)=TRUE by VALUAT_1:def 5;
      then Pj(c,x)=FALSE by MARGREL1:41;
      hence thesis by A10,MARGREL1:43;
    end;
    then Pj(B_INF(a 'imp' 'not' b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 19;
    hence thesis by BVFUNC_2:def 9;
end;

theorem
    All(b 'imp' 'not' c,PA,G) '&' Ex(a '&' c,PA,G) '<' Ex(a '&' 'not' b,PA,G)
proof
    let z be Element of Y;
    assume Pj(All(b 'imp' 'not' c,PA,G) '&' Ex(a '&' c,PA,G),z)=TRUE;
then A1:    Pj(All(b 'imp' 'not' c,PA,G),z) '&' Pj(Ex(a '&' c,PA,G),z)=TRUE
       by VALUAT_1:def 6;
A2:    now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b 'imp' 'not' c,x)=TRUE);
      then Pj(B_INF(b 'imp' 'not' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19
;
      then Pj(All(b 'imp' 'not' c,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(b 'imp' 'not' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a '&' c,x)=TRUE);
      then Pj(B_SUP(a '&' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(a '&' c,PA,G),z)=FALSE by BVFUNC_2:def 10;
      then Pj(Ex(a '&' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
    then consider x1 being Element of Y such that
      A3:x1 in EqClass(z,CompF(PA,G)) & Pj(a '&' c,x1)=TRUE;
      Pj(b 'imp' 'not' c,x1)=TRUE by A2,A3;
    then A4:('not' Pj(b,x1)) 'or' Pj('not' c,x1)=TRUE by BVFUNC_1:def 11;
A5:('not' Pj(b,x1))=TRUE or ('not' Pj(b,x1))=FALSE by MARGREL1:39;
A6:    Pj(a,x1) '&' Pj(c,x1)=TRUE by A3,VALUAT_1:def 6;
    per cases by A4,A5,A6,BINARITH:7,MARGREL1:45;
    suppose A7:(Pj(a,x1)=TRUE & Pj(c,x1)=TRUE) & ('not' Pj(b,x1))=TRUE;
      Pj(a '&' 'not' b,x1)
     =Pj(a,x1) '&' Pj('not' b,x1) by VALUAT_1:def 6
    .=TRUE '&' TRUE by A7,VALUAT_1:def 5
    .=TRUE by MARGREL1:45;
    then Pj(B_SUP(a '&' 'not' b,CompF(PA,G)),z) = TRUE by A3,BVFUNC_1:def 20;
    hence thesis by BVFUNC_2:def 10;
    suppose A8:(Pj(a,x1)=TRUE & Pj(c,x1)=TRUE) & Pj('not' c,x1)=TRUE;
    then 'not' Pj(c,x1)=TRUE by VALUAT_1:def 5;
    then Pj(c,x1)=FALSE by MARGREL1:41;
    hence thesis by A8,MARGREL1:43;
end;

theorem
    All(b 'imp' c,PA,G) '&' Ex(a '&' 'not' c,PA,G) '<' Ex(a '&' 'not' b,PA,G)
proof
    let z be Element of Y;
    assume Pj(All(b 'imp' c,PA,G) '&' Ex(a '&' 'not' c,PA,G),z)=TRUE;
then A1:    Pj(All(b 'imp' c,PA,G),z) '&' Pj(Ex(a '&' 'not' c,PA,G),z)=TRUE
       by VALUAT_1:def 6;
A2: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b 'imp' c,x)=TRUE);
      then Pj(B_INF(b 'imp' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(b 'imp' c,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(b 'imp' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(a '&' 'not' c,x)=TRUE);
      then Pj(B_SUP(a '&' 'not' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(a '&' 'not' c,PA,G),z)=FALSE by BVFUNC_2:def 10;
      then Pj(Ex(a '&' 'not' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
    then consider x1 being Element of Y such that
      A3:x1 in EqClass(z,CompF(PA,G)) & Pj(a '&' 'not' c,x1)=TRUE;
      Pj(b 'imp' c,x1)=TRUE by A2,A3;
    then A4:('not' Pj(b,x1)) 'or' Pj(c,x1)=TRUE by BVFUNC_1:def 11;
A5:('not' Pj(b,x1))=TRUE or ('not' Pj(b,x1))=FALSE by MARGREL1:39;
A6:    Pj(a,x1) '&' Pj('not' c,x1)=TRUE by A3,VALUAT_1:def 6;
    per cases by A4,A5,A6,BINARITH:7,MARGREL1:45;
    suppose A7:(Pj(a,x1)=TRUE & Pj('not' c,x1)=TRUE) & ('not' Pj(b,x1))=TRUE;
      Pj(a '&' 'not' b,x1) = Pj(a,x1) '&' Pj('not' b,x1) by VALUAT_1:def 6
    .=TRUE '&' TRUE by A7,VALUAT_1:def 5
    .=TRUE by MARGREL1:45;
    then Pj(B_SUP(a '&' 'not' b,CompF(PA,G)),z) = TRUE by A3,BVFUNC_1:def 20;
    hence thesis by BVFUNC_2:def 10;
    suppose A8:(Pj(a,x1)=TRUE & Pj('not' c,x1)=TRUE) & Pj(c,x1)=TRUE;
    then 'not' Pj(c,x1)=TRUE by VALUAT_1:def 5;
    then Pj(c,x1)=FALSE by MARGREL1:41;
    hence thesis by A8,MARGREL1:43;
end;

theorem
    Ex(c,PA,G) '&' All(c 'imp' b,PA,G) '&' All(c 'imp' a,PA,G)
   '<' Ex(a '&' b,PA,G)
proof
    let z be Element of Y;
    assume
      Pj(Ex(c,PA,G) '&' All(c 'imp' b,PA,G) '&' All(c 'imp' a,PA,G),z)=TRUE;
then A1: Pj(Ex(c,PA,G) '&' All(c 'imp' b,PA,G),z) '&' Pj(All(c 'imp' a,PA,G),z)
=TRUE
    by VALUAT_1:def 6;
    then Pj(Ex(c,PA,G),z) '&' Pj(All(c 'imp' b,PA,G),z) '&'
       Pj(All(c 'imp' a,PA,G),z)=TRUE by VALUAT_1:def 6;
then A2:(Pj(Ex(c,PA,G),z) '&' Pj(All(c 'imp' b,PA,G),z))=TRUE &
       Pj(All(c 'imp' a,PA,G),z)=TRUE by MARGREL1:45;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(c,x)=TRUE);
      then Pj(B_SUP(c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(c,PA,G),z)=FALSE by BVFUNC_2:def 10;
      then Pj(Ex(c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A2,MARGREL1:45;
    end;
    then consider x1 being Element of Y such that
A3:  x1 in EqClass(z,CompF(PA,G)) & Pj(c,x1)=TRUE;
      now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(c 'imp' a,x)=TRUE);
      then Pj(B_INF(c 'imp' a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(c 'imp' a,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(c 'imp' a,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
    then Pj(c 'imp' a,x1)=TRUE by A3;
    then A4:('not' Pj(c,x1)) 'or' Pj(a,x1)=TRUE by BVFUNC_1:def 11;
A5:    ('not' Pj(c,x1))=TRUE or
    ('not' Pj(c,x1))=FALSE by MARGREL1:39;
      now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(c 'imp' b,x)=TRUE);
      then Pj(B_INF(c 'imp' b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(c 'imp' b,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(c 'imp' b,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A2,MARGREL1:45;
    end;
    then Pj(c 'imp' b,x1)=TRUE by A3;
    then A6:('not' Pj(c,x1)) 'or' Pj(b,x1)=TRUE by BVFUNC_1:def 11;
    per cases by A4,A5,A6,BINARITH:7;
    suppose ('not' Pj(c,x1))=TRUE;
    then Pj(c,x1)=FALSE by MARGREL1:41;
    hence thesis by A3,MARGREL1:43;
    suppose ('not' Pj(c,x1))=TRUE & Pj(b,x1)=TRUE;
    then Pj(c,x1)=FALSE by MARGREL1:41;
    hence thesis by A3,MARGREL1:43;
    suppose Pj(a,x1)=TRUE & ('not' Pj(c,x1))=TRUE;
    then Pj(c,x1)=FALSE by MARGREL1:41;
    hence thesis by A3,MARGREL1:43;
    suppose Pj(a,x1)=TRUE & Pj(b,x1)=TRUE;
    then Pj(a '&' b,x1) =TRUE '&' TRUE by VALUAT_1:def 6
    .=TRUE by MARGREL1:45;
    then Pj(B_SUP(a '&' b,CompF(PA,G)),z) = TRUE by A3,BVFUNC_1:def 20;
    hence thesis by BVFUNC_2:def 10;
end;

theorem
    All(b 'imp' c,PA,G) '&' All(c 'imp' 'not' a,PA,G)
   '<' All(a 'imp' 'not' b,PA,G)
proof
    let z be Element of Y;
    assume Pj(All(b 'imp' c,PA,G) '&' All(c 'imp' 'not' a,PA,G),z)=TRUE;
then A1:    Pj(All(b 'imp' c,PA,G),z) '&' Pj(All(c 'imp' 'not' a,PA,G),z)=TRUE
       by VALUAT_1:def 6;
A2: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(c 'imp' 'not' a,x)=TRUE);
      then Pj(B_INF(c 'imp' 'not' a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19
;
      then Pj(All(c 'imp' 'not' a,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(c 'imp' 'not' a,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
A3: now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b 'imp' c,x)=TRUE);
      then Pj(B_INF(b 'imp' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(b 'imp' c,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(b 'imp' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
      for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(a 'imp' 'not' b,x)=TRUE
    proof
      let x be Element of Y;
      assume A4:x in EqClass(z,CompF(PA,G));
      then Pj(c 'imp' 'not' a,x)=TRUE by A2;
      then A5:('not' Pj(c,x)) 'or' Pj('not' a,x)=TRUE by BVFUNC_1:def 11;
A6:  ('not' Pj(c,x))=TRUE or ('not' Pj(c,x))=FALSE by MARGREL1:39;
        Pj(b 'imp' c,x)=TRUE by A3,A4;
      then A7:('not' Pj(b,x)) 'or' Pj(c,x)=TRUE by BVFUNC_1:def 11;
A8:  ('not' Pj(b,x))=TRUE or ('not' Pj(b,x))=FALSE by MARGREL1:39;
      per cases by A5,A6,A7,A8,BINARITH:7;
      suppose ('not' Pj(c,x))=TRUE & ('not' Pj(b,x))=TRUE;
      then Pj('not' b,x)=TRUE by VALUAT_1:def 5;
      hence Pj(a 'imp' 'not' b,x) =('not' Pj(a,x)) 'or' TRUE by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      suppose A9:('not' Pj(c,x))=TRUE & Pj(c,x)=TRUE;
      then Pj(c,x)=FALSE by MARGREL1:41;
      hence thesis by A9,MARGREL1:43;
      suppose Pj('not' a,x)=TRUE & ('not' Pj(b,x))=TRUE;
      then Pj('not' b,x)=TRUE by VALUAT_1:def 5;
      hence Pj(a 'imp' 'not' b,x) =('not' Pj(a,x)) 'or' TRUE by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
      suppose Pj('not' a,x)=TRUE & Pj(c,x)=TRUE;
      then 'not' Pj(a,x)=TRUE by VALUAT_1:def 5;
      hence Pj(a 'imp' 'not' b,x) =TRUE 'or' Pj('not' b,x) by BVFUNC_1:def 11
      .=TRUE by BINARITH:19;
    end;
    then Pj(B_INF(a 'imp' 'not' b,CompF(PA,G)),z) = TRUE by BVFUNC_1:def 19;
    hence thesis by BVFUNC_2:def 9;
end;

theorem
    Ex(b,PA,G) '&' All(b 'imp' c,PA,G) '&' All(c 'imp' a,PA,G)
   '<' Ex(a '&' b,PA,G)
proof
    let z be Element of Y;
    assume
      Pj(Ex(b,PA,G) '&' All(b 'imp' c,PA,G) '&' All(c 'imp' a,PA,G),z)=TRUE;
then A1:Pj(Ex(b,PA,G) '&' All(b 'imp' c,PA,G),z) '&' Pj(All(c 'imp' a,PA,G),z)=
TRUE
    by VALUAT_1:def 6;
    then Pj(Ex(b,PA,G),z) '&' Pj(All(b 'imp' c,PA,G),z) '&'
       Pj(All(c 'imp' a,PA,G),z)=TRUE by VALUAT_1:def 6;
then A2:(Pj(Ex(b,PA,G),z) '&' Pj(All(b 'imp' c,PA,G),z))=TRUE &
       Pj(All(c 'imp' a,PA,G),z)=TRUE by MARGREL1:45;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(b,x)=TRUE);
      then Pj(B_SUP(b,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(b,PA,G),z)=FALSE by BVFUNC_2:def 10;
      then Pj(Ex(b,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A2,MARGREL1:45;
    end;
    then consider x1 being Element of Y such that
A3:  x1 in EqClass(z,CompF(PA,G)) & Pj(b,x1)=TRUE;
      now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(c 'imp' a,x)=TRUE);
      then Pj(B_INF(c 'imp' a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(c 'imp' a,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(c 'imp' a,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
    then Pj(c 'imp' a,x1)=TRUE by A3;
    then A4:('not' Pj(c,x1)) 'or' Pj(a,x1)=TRUE by BVFUNC_1:def 11;
A5:('not' Pj(c,x1))=TRUE or ('not' Pj(c,x1))=FALSE by MARGREL1:39;
      now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b 'imp' c,x)=TRUE);
      then Pj(B_INF(b 'imp' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(b 'imp' c,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(b 'imp' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A2,MARGREL1:45;
    end;
    then Pj(b 'imp' c,x1)=TRUE by A3;
    then A6:('not' Pj(b,x1)) 'or' Pj(c,x1)=TRUE by BVFUNC_1:def 11;
A7:('not' Pj(b,x1))=TRUE or ('not' Pj(b,x1))=FALSE by MARGREL1:39;
    per cases by A4,A5,A6,A7,BINARITH:7;
    suppose ('not' Pj(c,x1))=TRUE & ('not' Pj(b,x1))=TRUE;
    then Pj(b,x1)=FALSE by MARGREL1:41;
    hence thesis by A3,MARGREL1:43;
    suppose A8:('not' Pj(c,x1))=TRUE & Pj(c,x1)=TRUE;
    then Pj(c,x1)=FALSE by MARGREL1:41;
    hence thesis by A8,MARGREL1:43;
    suppose Pj(a,x1)=TRUE & ('not' Pj(b,x1))=TRUE;
    then Pj(b,x1)=FALSE by MARGREL1:41;
    hence thesis by A3,MARGREL1:43;
    suppose Pj(a,x1)=TRUE & Pj(c,x1)=TRUE;
    then Pj(a '&' b,x1)
     =TRUE '&' TRUE by A3,VALUAT_1:def 6
    .=TRUE by MARGREL1:45;
    then Pj(B_SUP(a '&' b,CompF(PA,G)),z) = TRUE by A3,BVFUNC_1:def 20;
    hence thesis by BVFUNC_2:def 10;
end;

theorem
    Ex(c,PA,G) '&' All(b 'imp' 'not' c,PA,G) '&' All(c 'imp' a,PA,G)
   '<' Ex(a '&' 'not' b,PA,G)
proof
    let z be Element of Y;
    assume
      Pj(Ex(c,PA,G) '&' All(b 'imp' 'not'
c,PA,G) '&' All(c 'imp' a,PA,G),z)=TRUE;
then A1:    Pj(Ex(c,PA,G) '&' All(b 'imp' 'not' c,PA,G),z) '&'
    Pj(All(c 'imp' a,PA,G),z)=TRUE by VALUAT_1:def 6;
    then Pj(Ex(c,PA,G),z) '&' Pj(All(b 'imp' 'not' c,PA,G),z) '&'
       Pj(All(c 'imp' a,PA,G),z)=TRUE by VALUAT_1:def 6;
then A2:(Pj(Ex(c,PA,G),z) '&' Pj(All(b 'imp' 'not' c,PA,G),z))=TRUE &
       Pj(All(c 'imp' a,PA,G),z)=TRUE by MARGREL1:45;
      now assume not (ex x being Element of Y st
            x in EqClass(z,CompF(PA,G)) & Pj(c,x)=TRUE);
      then Pj(B_SUP(c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 20;
      then Pj(Ex(c,PA,G),z)=FALSE by BVFUNC_2:def 10;
      then Pj(Ex(c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A2,MARGREL1:45;
    end;
    then consider x1 being Element of Y such that
A3:  x1 in EqClass(z,CompF(PA,G)) & Pj(c,x1)=TRUE;
      now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(c 'imp' a,x)=TRUE);
      then Pj(B_INF(c 'imp' a,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19;
      then Pj(All(c 'imp' a,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(c 'imp' a,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A1,MARGREL1:45;
    end;
    then Pj(c 'imp' a,x1)=TRUE by A3;
    then A4:('not' Pj(c,x1)) 'or' Pj(a,x1)=TRUE by BVFUNC_1:def 11;
A5:('not' Pj(c,x1))=TRUE or ('not' Pj(c,x1))=FALSE by MARGREL1:39;
      now assume
        not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
         Pj(b 'imp' 'not' c,x)=TRUE);
      then Pj(B_INF(b 'imp' 'not' c,CompF(PA,G)),z) = FALSE by BVFUNC_1:def 19
;
      then Pj(All(b 'imp' 'not' c,PA,G),z)=FALSE by BVFUNC_2:def 9;
      then Pj(All(b 'imp' 'not' c,PA,G),z)<>TRUE by MARGREL1:43;
      hence contradiction by A2,MARGREL1:45;
    end;
    then Pj(b 'imp' 'not' c,x1)=TRUE by A3;
    then A6:('not' Pj(b,x1)) 'or' Pj('not' c,x1)=TRUE by BVFUNC_1:def 11;
A7:('not' Pj(b,x1))=TRUE or
    ('not' Pj(b,x1))=FALSE by MARGREL1:39;
    per cases by A4,A5,A6,A7,BINARITH:7;
    suppose ('not' Pj(c,x1))=TRUE & ('not' Pj(b,x1))=TRUE;
    then Pj(c,x1)=FALSE by MARGREL1:41;
    hence thesis by A3,MARGREL1:43;
    suppose ('not' Pj(c,x1))=TRUE & Pj('not' c,x1)=TRUE;
    then Pj(c,x1)=FALSE by MARGREL1:41;
    hence thesis by A3,MARGREL1:43;
    suppose A8:Pj(a,x1)=TRUE & ('not' Pj(b,x1))=TRUE;
      Pj(a '&' 'not' b,x1) =Pj(a,x1) '&' Pj('not' b,x1) by VALUAT_1:def 6
    .=TRUE '&' TRUE by A8,VALUAT_1:def 5
    .=TRUE by MARGREL1:45;
    then Pj(B_SUP(a '&' 'not' b,CompF(PA,G)),z)=TRUE by A3,BVFUNC_1:def 20;
    hence thesis by BVFUNC_2:def 10;
    suppose Pj(a,x1)=TRUE & Pj('not' c,x1)=TRUE;
    then 'not' Pj(c,x1)=TRUE by VALUAT_1:def 5;
    then Pj(c,x1)=FALSE by MARGREL1:41;
    hence thesis by A3,MARGREL1:43;
end;


Back to top