The Mizar article:

Propositional Calculus for Boolean Valued Functions. Part III

by
Shunichi Kobayashi

Received April 23, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: BVFUNC_7
[ MML identifier index ]


environ

 vocabulary FUNCT_2, MARGREL1, BVFUNC_1, ZF_LANG, FUNCT_1, RELAT_1, PARTIT1;
 notation TARSKI, XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, RELAT_1, FUNCT_1,
      FRAENKEL, BINARITH, BVFUNC_1;
 constructors BINARITH, BVFUNC_1;
 clusters MARGREL1, VALUAT_1, BINARITH, FRAENKEL;
 requirements SUBSET, BOOLE;
 definitions BVFUNC_1;
 theorems FUNCT_1, FUNCT_2, MARGREL1, BINARITH, BVFUNC_1, BVFUNC_4, VALUAT_1;

begin

::Chap. 1  Propositional Calculus

reserve Y for non empty set;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' ('not' a 'imp' b) = b
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj((a 'imp' b) '&' ('not' a 'imp' b),x) = Pj(b,x)
  proof
    let x be Element of Y;
A2:Pj((a 'imp' b) '&' ('not' a 'imp' b),x)
   =Pj(a 'imp' b,x) '&' Pj('not' a 'imp' b,x) by VALUAT_1:def 6
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' Pj('not' a 'imp' b,x) by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj('not'
a,x) 'or' Pj(b,x)) by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' 'not'
Pj(a,x) 'or' Pj(b,x)) by VALUAT_1:def 5
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' (Pj(a,x) 'or' Pj(b,x)) by MARGREL1:40;
      now per cases by MARGREL1:39;
     case Pj(a,x)=TRUE;
     then Pj((a 'imp' b) '&' ('not' a 'imp' b),x)
    =(FALSE 'or' Pj(b,x)) '&' (TRUE 'or' Pj(b,x)) by A2,MARGREL1:41
   .=(FALSE 'or' Pj(b,x)) '&' TRUE by BINARITH:19
   .=TRUE '&' Pj(b,x) by BINARITH:7
   .=Pj(b,x) by MARGREL1:50;
     hence thesis;
     case Pj(a,x)=FALSE;
     then Pj((a 'imp' b) '&' ('not' a 'imp' b),x)
    =(TRUE 'or' Pj(b,x)) '&' (FALSE 'or' Pj(b,x)) by A2,MARGREL1:41
   .=TRUE '&' (FALSE 'or' Pj(b,x)) by BINARITH:19
   .=TRUE '&' Pj(b,x) by BINARITH:7
   .=Pj(b,x) by MARGREL1:50;
     hence thesis;
    end;
    hence thesis;
  end;
  consider k3 being Function such that
    A3: ((a 'imp' b) '&' ('not' a 'imp' b))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A4: b=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A3,A4;
  hence ((a 'imp' b) '&' ('not' a 'imp' b))=b by A3,A4,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (a 'imp' 'not' b) = 'not' a
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj((a 'imp' b) '&' (a 'imp' 'not' b),x) = Pj('not' a,x)
  proof
    let x be Element of Y;
A2:Pj((a 'imp' b) '&' (a 'imp' 'not' b),x)
   =Pj(a 'imp' b,x) '&' Pj(a 'imp' 'not' b,x) by VALUAT_1:def 6
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' Pj(a 'imp' 'not' b,x) by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(a,x) 'or' Pj('not'
b,x)) by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(a,x) 'or' 'not'
Pj(b,x)) by VALUAT_1:def 5;
      now per cases by MARGREL1:39;
     case Pj(b,x)=TRUE;
     then Pj((a 'imp' b) '&' (a 'imp' 'not' b),x)
    =('not' Pj(a,x) 'or' TRUE) '&' ('not' Pj(a,x) 'or' FALSE) by A2,MARGREL1:41
   .=('not' Pj(a,x) 'or' TRUE) '&' 'not' Pj(a,x) by BINARITH:7
   .=TRUE '&' 'not' Pj(a,x) by BINARITH:19
   .='not' Pj(a,x) by MARGREL1:50
   .=Pj('not' a,x) by VALUAT_1:def 5;
     hence thesis;
     case Pj(b,x)=FALSE;
     then Pj((a 'imp' b) '&' (a 'imp' 'not' b),x)
    =('not' Pj(a,x) 'or' FALSE) '&' ('not' Pj(a,x) 'or' TRUE) by A2,MARGREL1:41
   .='not' Pj(a,x) '&' ('not' Pj(a,x) 'or' TRUE) by BINARITH:7
   .=TRUE '&' 'not' Pj(a,x) by BINARITH:19
   .='not' Pj(a,x) by MARGREL1:50
   .=Pj('not' a,x) by VALUAT_1:def 5;
     hence thesis;
    end;
    hence thesis;
  end;
  consider k3 being Function such that
    A3: ((a 'imp' b) '&' (a 'imp' 'not' b))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A4: 'not' a=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A3,A4;
  hence ((a 'imp' b) '&' (a 'imp' 'not' b))='not' a by A3,A4,FUNCT_1:9;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a 'imp' (b 'or' c) = (a 'imp' b) 'or' (a 'imp' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'imp' (b 'or' c),x) = Pj((a 'imp' b) 'or' (a 'imp' c),x)
  proof
    let x be Element of Y;
      Pj((a 'imp' b) 'or' (a 'imp' c),x)
   =Pj(a 'imp' b,x) 'or' Pj(a 'imp' c,x) by BVFUNC_1:def 7
  .=('not' Pj(a,x) 'or' Pj(b,x)) 'or' Pj(a 'imp' c,x) by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(b,x)) 'or' ('not'
Pj(a,x) 'or' Pj(c,x)) by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' ('not' Pj(a,x) 'or' Pj(b,x))) 'or' Pj(c,x)
  by BINARITH:20
  .=(('not' Pj(a,x) 'or' 'not' Pj(a,x)) 'or' Pj(b,x)) 'or' Pj(c,x)
  by BINARITH:20
  .=('not' Pj(a,x) 'or' Pj(b,x)) 'or' Pj(c,x) by BINARITH:21
  .='not' Pj(a,x) 'or' (Pj(b,x) 'or' Pj(c,x)) by BINARITH:20
  .='not' Pj(a,x) 'or' Pj(b 'or' c,x) by BVFUNC_1:def 7
  .=Pj(a 'imp' (b 'or' c),x) by BVFUNC_1:def 11;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'imp' (b 'or' c))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'imp' b) 'or' (a 'imp' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence (a 'imp' (b 'or' c))=(a 'imp' b) 'or' (a 'imp' c) by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a 'imp' (b '&' c) = (a 'imp' b) '&' (a 'imp' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'imp' (b '&' c),x) = Pj((a 'imp' b) '&' (a 'imp' c),x)
  proof
    let x be Element of Y;
      Pj((a 'imp' b) '&' (a 'imp' c),x)
   =Pj(a 'imp' b,x) '&' Pj(a 'imp' c,x) by VALUAT_1:def 6
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' Pj(a 'imp' c,x) by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not'
Pj(a,x) 'or' Pj(c,x)) by BVFUNC_1:def 11
  .='not' Pj(a,x) 'or' (Pj(b,x) '&' Pj(c,x)) by BINARITH:23
  .='not' Pj(a,x) 'or' (Pj(b '&' c,x)) by VALUAT_1:def 6
  .=Pj(a 'imp' (b '&' c),x) by BVFUNC_1:def 11;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'imp' (b '&' c))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'imp' b) '&' (a 'imp' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
    Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence (a 'imp' (b '&' c))=(a 'imp' b) '&' (a 'imp' c) by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'or' b) 'imp' c = (a 'imp' c) '&' (b 'imp' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj((a 'or' b) 'imp' c,x) = Pj((a 'imp' c) '&' (b 'imp' c),x)
  proof
    let x be Element of Y;
      Pj((a 'imp' c) '&' (b 'imp' c),x)
   =Pj(a 'imp' c,x) '&' Pj(b 'imp' c,x) by VALUAT_1:def 6
  .=('not' Pj(a,x) 'or' Pj(c,x)) '&' Pj(b 'imp' c,x) by BVFUNC_1:def 11
  .=(Pj(c,x) 'or' 'not' Pj(a,x)) '&' ('not'
Pj(b,x) 'or' Pj(c,x)) by BVFUNC_1:def 11
  .=Pj(c,x) 'or' ('not' Pj(a,x) '&' 'not' Pj(b,x)) by BINARITH:23
  .='not'( Pj(a,x) 'or' Pj(b,x)) 'or' Pj(c,x) by BINARITH:10
  .='not' Pj(a 'or' b,x) 'or' Pj(c,x) by BVFUNC_1:def 7
  .=Pj((a 'or' b) 'imp' c,x) by BVFUNC_1:def 11;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: ((a 'or' b) 'imp' c)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'imp' c) '&' (b 'imp' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence ((a 'or' b) 'imp' c)=(a 'imp' c) '&' (b 'imp' c) by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'imp' c = (a 'imp' c) 'or' (b 'imp' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj((a '&' b) 'imp' c,x) = Pj((a 'imp' c) 'or' (b 'imp' c),x)
  proof
    let x be Element of Y;
      Pj((a 'imp' c) 'or' (b 'imp' c),x)
   =Pj(a 'imp' c,x) 'or' Pj(b 'imp' c,x) by BVFUNC_1:def 7
  .=('not' Pj(a,x) 'or' Pj(c,x)) 'or' Pj(b 'imp' c,x) by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(c,x)) 'or' ('not'
Pj(b,x) 'or' Pj(c,x)) by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' (Pj(c,x) 'or' 'not' Pj(b,x))) 'or' Pj(c,x)
  by BINARITH:20
  .=(('not' Pj(a,x) 'or' 'not' Pj(b,x)) 'or' Pj(c,x)) 'or' Pj(c,x)
  by BINARITH:20
  .=('not' Pj(a,x) 'or' 'not' Pj(b,x)) 'or' (Pj(c,x) 'or' Pj(c,x))
  by BINARITH:20
  .=('not' Pj(a,x) 'or' 'not' Pj(b,x)) 'or' Pj(c,x) by BINARITH:21
  .='not'( Pj(a,x) '&' Pj(b,x)) 'or' Pj(c,x) by BINARITH:9
  .='not' Pj(a '&' b,x) 'or' Pj(c,x) by VALUAT_1:def 6
  .=Pj((a '&' b) 'imp' c,x) by BVFUNC_1:def 11;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: ((a '&' b) 'imp' c)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a 'imp' c) 'or' (b 'imp' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence ((a '&' b) 'imp' c)=(a 'imp' c) 'or' (b 'imp' c) by A2,A3,FUNCT_1:9;
end;

theorem Th7: for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'imp' c = a 'imp' (b 'imp' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj((a '&' b) 'imp' c,x) = Pj(a 'imp' (b 'imp' c),x)
  proof
    let x be Element of Y;
      Pj(a 'imp' (b 'imp' c),x)
   ='not' Pj(a,x) 'or' Pj(b 'imp' c,x) by BVFUNC_1:def 11
  .='not' Pj(a,x) 'or' ('not' Pj(b,x) 'or' Pj(c,x)) by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' 'not' Pj(b,x)) 'or' Pj(c,x) by BINARITH:20
  .='not'( Pj(a,x) '&' Pj(b,x)) 'or' Pj(c,x) by BINARITH:9
  .='not' Pj(a '&' b,x) 'or' Pj(c,x) by VALUAT_1:def 6
  .=Pj((a '&' b) 'imp' c,x) by BVFUNC_1:def 11;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: ((a '&' b) 'imp' c)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: a 'imp' (b 'imp' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence ((a '&' b) 'imp' c)=a 'imp' (b 'imp' c) by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'imp' c = a 'imp' ('not' b 'or' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj((a '&' b) 'imp' c,x) = Pj(a 'imp' ('not' b 'or' c),x)
  proof
    let x be Element of Y;
      Pj(a 'imp' ('not' b 'or' c),x)
   =Pj(a 'imp' (b 'imp' c),x) by BVFUNC_4:8;
    hence thesis by Th7;
  end;
  consider k3 being Function such that
    A2: ((a '&' b) 'imp' c)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: a 'imp' ('not' b 'or' c)=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence ((a '&' b) 'imp' c)=a 'imp' ('not' b 'or' c) by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a 'imp' (b 'or' c) = (a '&' 'not' b) 'imp' c
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'imp' (b 'or' c),x) = Pj((a '&' 'not' b) 'imp' c,x)
  proof
    let x be Element of Y;
      Pj((a '&' 'not' b) 'imp' c,x)
   ='not' Pj(a '&' 'not' b,x) 'or' Pj(c,x) by BVFUNC_1:def 11
  .='not'( Pj(a,x) '&' Pj('not' b,x)) 'or' Pj(c,x) by VALUAT_1:def 6
  .=('not' Pj(a,x) 'or' 'not' Pj('not' b,x)) 'or' Pj(c,x) by BINARITH:9
  .=('not' Pj(a,x) 'or' 'not' 'not' Pj(b,x)) 'or' Pj(c,x) by VALUAT_1:def 5
  .=('not' Pj(a,x) 'or' Pj(b,x)) 'or' Pj(c,x) by MARGREL1:40
  .='not' Pj(a,x) 'or' (Pj(b,x) 'or' Pj(c,x)) by BINARITH:20
  .='not' Pj(a,x) 'or' Pj(b 'or' c,x) by BVFUNC_1:def 7
  .=Pj(a 'imp' (b 'or' c),x) by BVFUNC_1:def 11;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'imp' (b 'or' c))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: (a '&' 'not' b) 'imp' c =k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence (a 'imp' (b 'or' c))=(a '&' 'not' b) 'imp' c by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a '&' (a 'imp' b) = a '&' b
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a '&' (a 'imp' b),x) = Pj(a '&' b,x)
  proof
    let x be Element of Y;
      Pj(a '&' (a 'imp' b),x)
   =Pj(a,x) '&' Pj(a 'imp' b,x) by VALUAT_1:def 6
  .=Pj(a,x) '&' ('not' Pj(a,x) 'or' Pj(b,x)) by BVFUNC_1:def 11
  .=(Pj(a,x) '&' 'not' Pj(a,x)) 'or' (Pj(a,x) '&' Pj(b,x)) by BINARITH:22
  .=FALSE 'or' (Pj(a,x) '&' Pj(b,x)) by MARGREL1:46
  .=Pj(a,x) '&' Pj(b,x) by BINARITH:7
  .=Pj(a '&' b,x) by VALUAT_1:def 6;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a '&' (a 'imp' b))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: a '&' b=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence (a '&' (a 'imp' b))=a '&' b by A2,A3,FUNCT_1:9;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' 'not' b = 'not' a '&' 'not' b
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj((a 'imp' b) '&' 'not' b,x) = Pj('not' a '&' 'not' b,x)
  proof
    let x be Element of Y;
      Pj((a 'imp' b) '&' 'not' b,x)
   =Pj(a 'imp' b,x) '&' Pj('not' b,x) by VALUAT_1:def 6
  .=Pj('not' b,x) '&' ('not' Pj(a,x) 'or' Pj(b,x)) by BVFUNC_1:def 11
  .=(Pj('not' b,x) '&' 'not' Pj(a,x)) 'or' (Pj('not'
b,x) '&' Pj(b,x)) by BINARITH:22
  .=(Pj('not' b,x) '&' 'not' Pj(a,x)) 'or' (Pj(b,x) '&' 'not'
Pj(b,x)) by VALUAT_1:def 5
  .=(Pj('not' b,x) '&' 'not' Pj(a,x)) 'or' FALSE by MARGREL1:46
  .=Pj('not' b,x) '&' 'not' Pj(a,x) by BINARITH:7
  .=Pj('not' b,x) '&' Pj('not' a,x) by VALUAT_1:def 5
  .=Pj('not' a '&' 'not' b,x) by VALUAT_1:def 6;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: ((a 'imp' b) '&' 'not' b)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: 'not' a '&' 'not' b=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence ((a 'imp' b) '&' 'not' b)='not' a '&' 'not' b by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '&' (b 'imp' c) = (a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj((a 'imp' b) '&' (b 'imp' c),x) =
   Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x)
  proof
    let x be Element of Y;
A2:Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x)
   =Pj((a 'imp' b) '&' (b 'imp' c),x) '&' Pj((a 'imp' c),x) by VALUAT_1:def 6
  .=(Pj(a 'imp' b,x) '&' Pj(b 'imp' c,x)) '&' Pj((a 'imp' c),x)
      by VALUAT_1:def 6
  .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' Pj(b 'imp' c,x)) '&' Pj((a 'imp' c),x)
      by BVFUNC_1:def 11
  .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not'
Pj(b,x) 'or' Pj(c,x))) '&' Pj((a 'imp' c),x)
      by BVFUNC_1:def 11
  .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x)))
    '&' ('not' Pj(a,x) 'or' Pj(c,x)) by BVFUNC_1:def 11
  .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' 'not'
Pj(a,x) 'or'
    (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' Pj(c,x)
   by BINARITH:22;
A3:Pj((a 'imp' b) '&' (b 'imp' c),x)
   =Pj(a 'imp' b,x) '&' Pj(b 'imp' c,x) by VALUAT_1:def 6
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' Pj(b 'imp' c,x)
      by BVFUNC_1:def 11
  .=('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))
      by BVFUNC_1:def 11;
A4:(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x)))
   =(Pj(a 'imp' b,x) '&' ('not' Pj(b,x) 'or' Pj(c,x)))
   by BVFUNC_1:def 11
  .=Pj(a 'imp' b,x) '&' Pj(b 'imp' c,x)
   by BVFUNC_1:def 11
  .=Pj((a 'imp' b) '&' (b 'imp' c),x) by VALUAT_1:def 6;
      now per cases by MARGREL1:39;
     case Pj(a,x)=TRUE & Pj(c,x)=TRUE;
     then Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x)
   =(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not'
Pj(b,x) 'or' Pj(c,x))) '&' FALSE 'or'
    (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' TRUE
   by A2,MARGREL1:41
  .=FALSE 'or' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not'
Pj(b,x) 'or' Pj(c,x))) '&' TRUE
   by MARGREL1:49
  .=FALSE 'or' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x)))
   by MARGREL1:50
  .=Pj((a 'imp' b) '&' (b 'imp' c),x) by A4,BINARITH:7;
     hence thesis;
     case A5:Pj(a,x)=TRUE & Pj(c,x)=FALSE;
     then A6:Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x)
   =(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not'
Pj(b,x) 'or' Pj(c,x))) '&' FALSE 'or'
    (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' FALSE
   by A2,MARGREL1:41
  .=FALSE '&' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x)
  'or' Pj(c,x))) by BINARITH:21
  .=FALSE by MARGREL1:49;
    Pj((a 'imp' b) '&' (b 'imp' c),x)
   =(FALSE 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' FALSE) by A3,A5,MARGREL1:41
  .=(FALSE 'or' Pj(b,x)) '&' 'not' Pj(b,x) by BINARITH:7
  .=Pj(b,x) '&' 'not' Pj(b,x) by BINARITH:7
  .=FALSE by MARGREL1:46;
     hence thesis by A6;
     case Pj(a,x)=FALSE & Pj(c,x)=TRUE;
     then Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x)
   =(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not'
Pj(b,x) 'or' Pj(c,x))) '&' TRUE 'or'
    (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) '&' TRUE
   by A2,MARGREL1:41
  .=TRUE '&' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x)))
by BINARITH:21
  .=Pj((a 'imp' b) '&' (b 'imp' c),x) by A4,MARGREL1:50;
     hence thesis;
     case Pj(a,x)=FALSE & Pj(c,x)=FALSE;
     then Pj((a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c),x)
   =TRUE '&' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not'
Pj(b,x) 'or' Pj(c,x))) 'or'
    FALSE '&' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not'
Pj(b,x) 'or' Pj(c,x))) by A2,MARGREL1:41
  .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) 'or'
    FALSE '&' (('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x)))
   by MARGREL1:50
  .=(('not' Pj(a,x) 'or' Pj(b,x)) '&' ('not' Pj(b,x) 'or' Pj(c,x))) 'or' FALSE
   by MARGREL1:49
  .=Pj((a 'imp' b) '&' (b 'imp' c),x) by A4,BINARITH:7;
     hence thesis;
    end;
    hence thesis;
  end;
  consider k3 being Function such that
    A7: ((a 'imp' b) '&' (b 'imp' c))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A8: (a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c)=
          k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A7,A8;
  hence ((a 'imp' b) '&' (b 'imp' c))=
        (a 'imp' b) '&' (b 'imp' c) '&' (a 'imp' c) by A7,A8,FUNCT_1:9;
end;

theorem for a being Element of Funcs(Y,BOOLEAN) holds
I_el(Y) 'imp' a = a
proof
  let a be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(I_el(Y) 'imp' a,x) = Pj(a,x)
  proof
    let x be Element of Y;
      Pj(I_el(Y) 'imp' a,x)
   ='not' Pj(I_el(Y),x) 'or' Pj(a,x) by BVFUNC_1:def 11
  .='not' TRUE 'or' Pj(a,x) by BVFUNC_1:def 14
  .=FALSE 'or' Pj(a,x) by MARGREL1:41;
    hence thesis by BINARITH:7;
  end;
  consider k3 being Function such that
    A2: (I_el(Y) 'imp' a)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: a=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence (I_el(Y) 'imp' a)=a by A2,A3,FUNCT_1:9;
end;

theorem for a being Element of Funcs(Y,BOOLEAN) holds
a 'imp' O_el(Y) = 'not' a
proof
  let a be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'imp' O_el(Y),x) = Pj('not' a,x)
  proof
    let x be Element of Y;
      Pj(a 'imp' O_el(Y),x)
   ='not' Pj(a,x) 'or' Pj(O_el(Y),x) by BVFUNC_1:def 11
  .='not' Pj(a,x) 'or' FALSE by BVFUNC_1:def 13
  .='not' Pj(a,x) by BINARITH:7;
    hence thesis by VALUAT_1:def 5;
  end;
  consider k3 being Function such that
    A2: (a 'imp' O_el(Y))=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: 'not' a=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence (a 'imp' O_el(Y))='not' a by A2,A3,FUNCT_1:9;
end;

theorem for a being Element of Funcs(Y,BOOLEAN) holds
O_el(Y) 'imp' a = I_el(Y)
proof
  let a be Element of Funcs(Y,BOOLEAN);
    for x being Element of Y holds
   Pj(O_el(Y) 'imp' a,x) = TRUE
  proof
    let x be Element of Y;
      Pj(O_el(Y) 'imp' a,x)
   ='not' Pj(O_el(Y),x) 'or' Pj(a,x) by BVFUNC_1:def 11
  .='not' FALSE 'or' Pj(a,x) by BVFUNC_1:def 13
  .=TRUE 'or' Pj(a,x) by MARGREL1:41;
    hence thesis by BINARITH:19;
  end;
  hence thesis by BVFUNC_1:def 14;
end;

theorem for a being Element of Funcs(Y,BOOLEAN) holds
a 'imp' I_el(Y) = I_el(Y)
proof
  let a be Element of Funcs(Y,BOOLEAN);
    for x being Element of Y holds
   Pj(a 'imp' I_el(Y),x) = TRUE
  proof
    let x be Element of Y;
      Pj(a 'imp' I_el(Y),x)
   ='not' Pj(a,x) 'or' Pj(I_el(Y),x) by BVFUNC_1:def 11
  .='not' Pj(a,x) 'or' TRUE by BVFUNC_1:def 14;
    hence thesis by BINARITH:19;
  end;
  hence thesis by BVFUNC_1:def 14;
end;

theorem for a being Element of Funcs(Y,BOOLEAN) holds
a 'imp' 'not' a = 'not' a
proof
  let a be Element of Funcs(Y,BOOLEAN);
  A1:for x being Element of Y holds
   Pj(a 'imp' 'not' a,x) = Pj('not' a,x)
  proof
    let x be Element of Y;
      Pj(a 'imp' 'not' a,x)
   ='not' Pj(a,x) 'or' Pj('not' a,x) by BVFUNC_1:def 11
  .=Pj('not' a,x) 'or' Pj('not' a,x) by VALUAT_1:def 5
  .=Pj('not' a,x) by BINARITH:21;
    hence thesis;
  end;
  consider k3 being Function such that
    A2: (a 'imp' 'not' a)=k3 & dom k3=Y & rng k3 c= BOOLEAN
                     by FUNCT_2:def 2;
  consider k4 being Function such that
    A3: 'not' a=k4 & dom k4=Y & rng k4 c= BOOLEAN
                     by FUNCT_2:def 2;
     Y=dom k3 & Y=dom k4 & (for u being set
            st u in Y holds k3.u=k4.u)by A1,A2,A3;
  hence (a 'imp' 'not' a)='not' a by A2,A3,FUNCT_1:9;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) '<' (c 'imp' a) 'imp' (c 'imp' b)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
    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: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
      now per cases by A1,A2,BINARITH:7;
     case A3:'not' Pj(a,z)=TRUE;
       Pj((c 'imp' a) 'imp' (c 'imp' b),z)
    ='not' Pj(c 'imp' a,z) 'or' Pj(c 'imp' b,z) by BVFUNC_1:def 11
   .='not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' Pj(c 'imp' b,z) by BVFUNC_1:def 11
   .=('not' 'not' Pj(c,z) '&' TRUE) 'or' Pj(c 'imp' b,z) by A3,BINARITH:10
   .=(TRUE '&' Pj(c,z)) 'or' Pj(c 'imp' b,z) by MARGREL1:40
   .=Pj(c,z) 'or' Pj(c 'imp' b,z) by MARGREL1:50
   .=Pj(c,z) 'or' ('not' Pj(c,z) 'or' Pj(b,z)) by BVFUNC_1:def 11
   .=(Pj(c,z) 'or' 'not' Pj(c,z)) 'or' Pj(b,z) by BINARITH:20
   .=TRUE 'or' Pj(b,z) by BINARITH:18
   .=TRUE by BINARITH:19;
     hence thesis;
     case A4:Pj(b,z)=TRUE;
       Pj((c 'imp' a) 'imp' (c 'imp' b),z)
    ='not' Pj(c 'imp' a,z) 'or' Pj(c 'imp' b,z) by BVFUNC_1:def 11
   .='not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' Pj(c 'imp' b,z) by BVFUNC_1:def 11
   .='not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' ('not'
Pj(c,z) 'or' TRUE) by A4,BVFUNC_1:def 11
   .='not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' TRUE by BINARITH:19
   .=TRUE by BINARITH:19;
     hence thesis;
    end;
    hence thesis;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) '<' (a 'eqv' c) 'eqv' (b 'eqv' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume A1:Pj(a 'eqv' b,z)=TRUE;
      Pj(a 'eqv' b,z)
   =Pj((a 'imp' b) '&' (b 'imp' a),z) by BVFUNC_4:7
  .=Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z) by VALUAT_1:def 6;
then A2:Pj(a 'imp' b,z)=TRUE & Pj(b 'imp' a,z)=TRUE by A1,MARGREL1:45;
    then A3:'not' Pj(a,z) 'or' Pj(b,z) = TRUE by BVFUNC_1:def 11;
    A4: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
    A5: Pj(b 'imp' a,z) = 'not' Pj(b,z) 'or' Pj(a,z) by BVFUNC_1:def 11;
      Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
then A6:'not' Pj(b,z)=TRUE or Pj(a,z)=TRUE by A2,A5,BINARITH:7;
A7:Pj((a 'eqv' c) 'eqv' (b 'eqv' c),z)
  =(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(a,z))) 'or'
     (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or'
     (('not' Pj(a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z))))
    proof
      Pj((a 'eqv' c) 'eqv' (b 'eqv' c),z)
   =Pj(((a 'eqv' c) 'imp' (b 'eqv' c)) '&' ((b 'eqv' c) 'imp' (a 'eqv' c)),z)
   by BVFUNC_4:7
  .=Pj((((a 'imp' c) '&' (c 'imp' a)) 'imp' (b 'eqv' c)) '&'
    ((b 'eqv' c) 'imp' (a 'eqv' c)),z)
   by BVFUNC_4:7
  .=Pj((((a 'imp' c) '&' (c 'imp' a)) 'imp' (b 'imp' c) '&' (c 'imp' b)) '&'
    ((b 'eqv' c) 'imp' (a 'eqv' c)),z)
   by BVFUNC_4:7
  .=Pj((((a 'imp' c) '&' (c 'imp' a)) 'imp' (b 'imp' c) '&' (c 'imp' b)) '&'
    (((b 'imp' c) '&' (c 'imp' b)) 'imp' (a 'eqv' c)),z)
   by BVFUNC_4:7
  .=Pj((((a 'imp' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&'
       (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z)
   by BVFUNC_4:7
  .=Pj(((('not'
a 'or' c) '&' (c 'imp' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&'
       (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z)
   by BVFUNC_4:8
  .=Pj(((('not' a 'or' c) '&' ('not'
c 'or' a)) 'imp' ((b 'imp' c) '&' (c 'imp' b))) '&'
       (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z)
   by BVFUNC_4:8
  .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp' (('not'
b 'or' c) '&' (c 'imp' b))) '&'
       (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z)
   by BVFUNC_4:8
  .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp'
  (('not' b 'or' c) '&' ('not'
c 'or' b))) '&'
       (((b 'imp' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z)
   by BVFUNC_4:8
  .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp'
  (('not' b 'or' c) '&' ('not' c 'or' b))) '&' ((('not'
b 'or' c) '&' (c 'imp' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z)
   by BVFUNC_4:8
  .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp'
  (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       ((('not' b 'or' c) '&' ('not'
c 'or' b)) 'imp' ((a 'imp' c) '&' (c 'imp' a))),z) by BVFUNC_4:8
  .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp'
  (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       ((('not' b 'or' c) '&' ('not' c 'or' b)) 'imp' (('not'
a 'or' c) '&' (c 'imp' a))),z) by BVFUNC_4:8
  .=Pj(((('not' a 'or' c) '&' ('not' c 'or' a)) 'imp'
  (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       ((('not' b 'or' c) '&' ('not' c 'or' b)) 'imp'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_4:8
  .=Pj(('not'( ('not' a 'or' c) '&' ('not' c 'or' a))
  'or' (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       ((('not' b 'or' c) '&' ('not' c 'or' b)) 'imp'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_4:8
  .=Pj(('not'( ('not' a 'or' c) '&' ('not' c 'or' a)) 'or'
  (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       ('not'( ('not' b 'or' c) '&' ('not' c 'or' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_4:8
  .=Pj((('not'( 'not' a 'or' c) 'or' 'not'( 'not' c 'or' a)) 'or'
       (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       ('not'( ('not' b 'or' c) '&' ('not' c 'or' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_1:17
  .=Pj((('not'( 'not' a 'or' c) 'or' 'not'( 'not' c 'or' a)) 'or'
       (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       (('not'( 'not' b 'or' c) 'or' 'not'( 'not' c 'or' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_1:17
  .=Pj(((('not' 'not' a '&' 'not' c) 'or' 'not'( 'not' c 'or' a)) 'or'
       (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       (('not'( 'not' b 'or' c) 'or' 'not'( 'not' c 'or' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_1:16
  .=Pj(((('not' 'not' a '&' 'not' c) 'or' ('not' 'not' c '&' 'not' a)) 'or'
       (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       (('not'( 'not' b 'or' c) 'or' 'not'( 'not' c 'or' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_1:16
  .=Pj(((('not' 'not' a '&' 'not' c) 'or' ('not' 'not' c '&' 'not' a)) 'or'
       (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       ((('not' 'not' b '&' 'not' c) 'or' 'not'( 'not' c 'or' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_1:16
  .=Pj(((('not' 'not' a '&' 'not' c) 'or' ('not' 'not' c '&' 'not' a)) 'or'
       (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       ((('not' 'not' b '&' 'not' c) 'or' ('not' 'not' c '&' 'not' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_1:16
  .=Pj((((a '&' 'not' c) 'or' ('not' 'not' c '&' 'not' a)) 'or'
       (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       ((('not' 'not' b '&' 'not' c) 'or' ('not' 'not' c '&' 'not' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_1:4
  .=Pj((((a '&' 'not' c) 'or' (c '&' 'not' a)) 'or'
       (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       ((('not' 'not' b '&' 'not' c) 'or' ('not' 'not' c '&' 'not' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_1:4
  .=Pj((((a '&' 'not' c) 'or' (c '&' 'not' a)) 'or'
       (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       (((b '&' 'not' c) 'or' ('not' 'not' c '&' 'not' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_1:4
  .=Pj((((a '&' 'not' c) 'or' (c '&' 'not' a)) 'or'
       (('not' b 'or' c) '&' ('not' c 'or' b))) '&'
       (((b '&' 'not' c) 'or' (c '&' 'not' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a))),z)
   by BVFUNC_1:4
  .=Pj(((a '&' 'not' c) 'or' (c '&' 'not' a)) 'or'
       (('not' b 'or' c) '&' ('not' c 'or' b)),z) '&'
    Pj(((b '&' 'not' c) 'or' (c '&' 'not' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a)),z)
   by VALUAT_1:def 6
  .=(Pj((a '&' 'not' c) 'or' (c '&' 'not' a),z) 'or'
     Pj(('not' b 'or' c) '&' ('not' c 'or' b),z)) '&'
    Pj(((b '&' 'not' c) 'or' (c '&' 'not' b)) 'or'
       (('not' a 'or' c) '&' ('not' c 'or' a)),z)
   by BVFUNC_1:def 7
  .=(Pj((a '&' 'not' c) 'or' (c '&' 'not' a),z) 'or'
     Pj(('not' b 'or' c) '&' ('not' c 'or' b),z)) '&'
    (Pj((b '&' 'not' c) 'or' (c '&' 'not' b),z) 'or'
     Pj(('not' a 'or' c) '&' ('not' c 'or' a),z))
   by BVFUNC_1:def 7
  .=((Pj(a '&' 'not' c,z) 'or' Pj(c '&' 'not' a,z)) 'or'
     Pj(('not' b 'or' c) '&' ('not' c 'or' b),z)) '&'
    (Pj((b '&' 'not' c) 'or' (c '&' 'not' b),z) 'or'
     Pj(('not' a 'or' c) '&' ('not' c 'or' a),z))
   by BVFUNC_1:def 7
  .=((Pj(a '&' 'not' c,z) 'or' Pj(c '&' 'not' a,z)) 'or'
     (Pj('not' b 'or' c,z) '&' Pj('not' c 'or' b,z))) '&'
    (Pj((b '&' 'not' c) 'or' (c '&' 'not' b),z) 'or'
     Pj(('not' a 'or' c) '&' ('not' c 'or' a),z))
   by VALUAT_1:def 6
  .=((Pj(a '&' 'not' c,z) 'or' Pj(c '&' 'not' a,z)) 'or'
     (Pj('not' b 'or' c,z) '&' Pj('not' c 'or' b,z))) '&'
    ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or'
     Pj(('not' a 'or' c) '&' ('not' c 'or' a),z))
   by BVFUNC_1:def 7
  .=((Pj(a '&' 'not' c,z) 'or' Pj(c '&' 'not' a,z)) 'or'
     (Pj('not' b 'or' c,z) '&' Pj('not' c 'or' b,z))) '&'
    ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or'
     (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z)))
   by VALUAT_1:def 6
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' Pj(c '&' 'not' a,z)) 'or'
     (Pj('not' b 'or' c,z) '&' Pj('not' c 'or' b,z))) '&'
    ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or'
     (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z)))
   by VALUAT_1:def 6
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or'
     (Pj('not' b 'or' c,z) '&' Pj('not' c 'or' b,z))) '&'
    ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or'
     (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z)))
   by VALUAT_1:def 6
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or'
     ((Pj('not' b,z) 'or' Pj(c,z)) '&' Pj('not' c 'or' b,z))) '&'
    ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or'
     (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z)))
   by BVFUNC_1:def 7
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or'
     ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    ((Pj(b '&' 'not' c,z) 'or' Pj(c '&' 'not' b,z)) 'or'
     (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z)))
   by BVFUNC_1:def 7
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or'
     ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' Pj(c '&' 'not' b,z)) 'or'
     (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z)))
   by VALUAT_1:def 6
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or'
     ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' b,z))) 'or'
     (Pj('not' a 'or' c,z) '&' Pj('not' c 'or' a,z)))
   by VALUAT_1:def 6
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or'
     ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' b,z))) 'or'
     ((Pj('not' a,z) 'or' Pj(c,z)) '&' Pj('not' c 'or' a,z)))
   by BVFUNC_1:def 7
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' a,z))) 'or'
     ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' b,z))) 'or'
     ((Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z))))
   by BVFUNC_1:def 7
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(a,z))) 'or'
     ((Pj('not' b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' b,z))) 'or'
     ((Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z))))
   by VALUAT_1:def 5
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(a,z))) 'or'
     (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' Pj('not' b,z))) 'or'
     ((Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z))))
   by VALUAT_1:def 5
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(a,z))) 'or'
     (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or'
     ((Pj('not' a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z))))
   by VALUAT_1:def 5
  .=(((Pj(a,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(a,z))) 'or'
     (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or'
     (('not' Pj(a,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(a,z))))
   by VALUAT_1:def 5;
     hence thesis;
   end;
      now per cases by A3,A4,BINARITH:7;
    case A8:'not' Pj(a,z)=TRUE;
     then A9:Pj(a,z)=FALSE by MARGREL1:41;
     then Pj((a 'eqv' c) 'eqv' (b 'eqv' c),z)
   =((FALSE 'or' (Pj(c,z) '&' TRUE)) 'or'
     (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or'
     ((TRUE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' FALSE)))
   by A7,A8,MARGREL1:49
  .=((FALSE 'or' Pj(c,z)) 'or'
     (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or'
     ((TRUE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' FALSE)))
   by MARGREL1:50
  .=(Pj(c,z) 'or'
     (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or'
     ((TRUE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' FALSE)))
   by BINARITH:7
  .=(Pj(c,z) 'or'
     (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or'
     ((TRUE 'or' Pj(c,z)) '&' Pj('not' c,z)))
   by BINARITH:7
  .=(Pj(c,z) 'or'
     (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not' Pj(b,z))) 'or'
     (TRUE '&' Pj('not' c,z)))
   by BINARITH:19
  .=(Pj(c,z) 'or' (('not' Pj(b,z) 'or' Pj(c,z)) '&' (Pj('not'
c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not'
    Pj(b,z))) 'or' Pj('not' c,z))
   by MARGREL1:50
  .=((Pj(c,z) 'or' (Pj(c,z) 'or' 'not' Pj(b,z))) '&'
     (Pj(c,z) 'or' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not'
    Pj(b,z))) 'or' Pj('not' c,z)) by BINARITH:23
  .=(((Pj(c,z) 'or' Pj(c,z)) 'or' 'not' Pj(b,z)) '&'
     (Pj(c,z) 'or' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not'
    Pj(b,z))) 'or' Pj('not' c,z)) by BINARITH:20
  .=((Pj(c,z) 'or' 'not' Pj(b,z)) '&'
     (Pj(c,z) 'or' (Pj('not' c,z) 'or' Pj(b,z)))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not'
    Pj(b,z))) 'or' Pj('not' c,z))
   by BINARITH:21
  .=((Pj(c,z) 'or' 'not' Pj(b,z)) '&'
     ((Pj(c,z) 'or' Pj('not' c,z)) 'or' Pj(b,z))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not'
    Pj(b,z))) 'or' Pj('not' c,z)) by BINARITH:20
  .=((Pj(c,z) 'or' 'not' Pj(b,z)) '&'
     ((Pj(c,z) 'or' 'not' Pj(c,z)) 'or' Pj(b,z))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not'
    Pj(b,z))) 'or' Pj('not' c,z)) by VALUAT_1:def 5
  .=((Pj(c,z) 'or' 'not' Pj(b,z)) '&'
     (TRUE 'or' Pj(b,z))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not'
    Pj(b,z))) 'or' Pj('not' c,z)) by BINARITH:18
  .=(TRUE '&' (Pj(c,z) 'or' 'not' Pj(b,z))) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' 'not'
    Pj(b,z))) 'or' Pj('not' c,z)) by BINARITH:19
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    (((Pj(b,z) '&' Pj('not' c,z)) 'or'
    (Pj(c,z) '&' 'not' Pj(b,z))) 'or' Pj('not' c,z))
   by MARGREL1:50
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    ((Pj(b,z) '&' Pj('not' c,z)) 'or' (Pj('not' c,z) 'or'
    (Pj(c,z) '&' 'not' Pj(b,z)))) by BINARITH:20
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    ((Pj(b,z) '&' Pj('not' c,z)) 'or'
    ((Pj('not' c,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' 'not' Pj(b,z))))
   by BINARITH:23
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    ((Pj(b,z) '&' Pj('not' c,z)) 'or'
    (('not' Pj(c,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' 'not' Pj(b,z))))
   by VALUAT_1:def 5
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    ((Pj(b,z) '&' Pj('not' c,z)) 'or'
    (TRUE '&' (Pj('not' c,z) 'or' 'not' Pj(b,z))))
   by BINARITH:18
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    ((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' (Pj(b,z) '&' Pj('not'
c,z))) by MARGREL1:50
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    (((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' Pj(b,z)) '&'
     ((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' Pj('not' c,z)))
   by BINARITH:23
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    ((Pj('not' c,z) 'or' ('not' Pj(b,z) 'or' Pj(b,z))) '&'
     ((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' Pj('not' c,z)))
   by BINARITH:20
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    ((Pj('not' c,z) 'or' TRUE) '&'
     ((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' Pj('not' c,z)))
   by BINARITH:18
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    (TRUE '&' ((Pj('not' c,z) 'or' 'not' Pj(b,z)) 'or' Pj('not' c,z)))
   by BINARITH:19
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    (('not' Pj(b,z) 'or' Pj('not' c,z)) 'or' Pj('not' c,z)) by MARGREL1:50
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&'
    ('not' Pj(b,z) 'or' (Pj('not' c,z) 'or' Pj('not' c,z)))
   by BINARITH:20
  .=(Pj(c,z) 'or' 'not' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj('not' c,z))
   by BINARITH:21
  .=('not' Pj(b,z) '&' (Pj(c,z) 'or' 'not' Pj(b,z))) 'or'
    ((Pj(c,z) 'or' 'not' Pj(b,z)) '&' Pj('not' c,z)) by BINARITH:22
  .=(('not' Pj(b,z) '&' Pj(c,z)) 'or' ('not' Pj(b,z) '&' 'not' Pj(b,z))) 'or'
    (Pj('not' c,z) '&' (Pj(c,z) 'or' 'not' Pj(b,z)))
   by BINARITH:22
  .=(('not' Pj(b,z) '&' Pj(c,z)) 'or' 'not' Pj(b,z)) 'or'
    (Pj('not' c,z) '&' (Pj(c,z) 'or' 'not' Pj(b,z)))
   by BINARITH:16
  .=(('not' Pj(b,z) '&' Pj(c,z)) 'or' 'not' Pj(b,z)) 'or'
    (Pj('not' c,z) '&' Pj(c,z) 'or' Pj('not' c,z) '&' 'not' Pj(b,z))
   by BINARITH:22
  .=(('not' Pj(b,z) '&' Pj(c,z)) 'or' 'not' Pj(b,z)) 'or'
    ((Pj(c,z) '&' 'not' Pj(c,z)) 'or' (Pj('not' c,z) '&' 'not'
Pj(b,z))) by VALUAT_1:def 5
  .=(('not' Pj(b,z) '&' Pj(c,z)) 'or' 'not' Pj(b,z)) 'or'
    (FALSE 'or' (Pj('not' c,z) '&' 'not' Pj(b,z)))
   by MARGREL1:46
  .=('not' Pj(b,z) 'or' ('not' Pj(b,z) '&' Pj(c,z))) 'or'
    (Pj('not' c,z) '&' 'not' Pj(b,z)) by BINARITH:7
  .='not' Pj(b,z) 'or' (('not' Pj(b,z) '&' Pj(c,z)) 'or'
    (Pj('not' c,z) '&' 'not' Pj(b,z)))
   by BINARITH:20
  .=TRUE by A6,A9,BINARITH:19,MARGREL1:43;
    hence thesis;
    case A10:Pj(b,z)=TRUE;
    then 'not' Pj(b,z)=FALSE by MARGREL1:41;
    then Pj((a 'eqv' c) 'eqv' (b 'eqv' c),z)
   =((Pj('not' c,z) 'or' (Pj(c,z) '&' FALSE)) 'or'
     ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) '&'
    (((TRUE '&' Pj('not' c,z)) 'or' (Pj(c,z) '&' FALSE)) 'or'
     ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE)))
   by A6,A7,A10,MARGREL1:43,50
  .=((Pj('not' c,z) 'or' (FALSE '&' Pj(c,z))) 'or'
     ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) '&'
    ((Pj('not' c,z) 'or' (Pj(c,z) '&' FALSE)) 'or'
     ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) by MARGREL1:50
  .=((Pj('not' c,z) 'or' FALSE) 'or'
     ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) '&'
    ((Pj('not' c,z) 'or' (FALSE '&' Pj(c,z))) 'or'
     ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE)))
   by MARGREL1:49
  .=((Pj('not' c,z) 'or' FALSE) 'or'
     ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE))) '&'
    ((Pj('not' c,z) 'or' FALSE) 'or'
     ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE)))
   by MARGREL1:49
  .=((Pj('not' c,z) 'or' FALSE) 'or'
     ((FALSE 'or' Pj(c,z)) '&' TRUE)) '&'
    ((Pj('not' c,z) 'or' FALSE) 'or'
     ((FALSE 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' TRUE)))
   by BINARITH:19
  .=((Pj('not' c,z) 'or' FALSE) 'or'
     ((FALSE 'or' Pj(c,z)) '&' TRUE)) '&'
    ((Pj('not' c,z) 'or' FALSE) 'or'
     ((FALSE 'or' Pj(c,z)) '&' TRUE))
   by BINARITH:19
  .=((Pj('not' c,z) 'or' FALSE) 'or'
     (Pj(c,z) '&' TRUE)) '&'
    ((Pj('not' c,z) 'or' FALSE) 'or'
     ((FALSE 'or' Pj(c,z)) '&' TRUE))
   by BINARITH:7
  .=((Pj('not' c,z) 'or' FALSE) 'or'
     (Pj(c,z) '&' TRUE)) '&'
    ((Pj('not' c,z) 'or' FALSE) 'or'
     (Pj(c,z) '&' TRUE))
   by BINARITH:7
  .=(Pj('not' c,z) 'or'
     (Pj(c,z) '&' TRUE)) '&'
    ((Pj('not' c,z) 'or' FALSE) 'or'
     (Pj(c,z) '&' TRUE))
   by BINARITH:7
  .=(Pj('not' c,z) 'or' (TRUE '&' Pj(c,z))) '&'
    (Pj('not' c,z) 'or' (Pj(c,z) '&' TRUE)) by BINARITH:7
  .=(Pj('not' c,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' (TRUE '&' Pj(c,z)))
   by MARGREL1:50
  .=(Pj('not' c,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(c,z))
   by MARGREL1:50
  .=('not' Pj(c,z) 'or' Pj(c,z)) '&' (Pj('not' c,z) 'or' Pj(c,z))
   by VALUAT_1:def 5
  .=('not' Pj(c,z) 'or' Pj(c,z)) '&' ('not' Pj(c,z) 'or' Pj(c,z))
   by VALUAT_1:def 5
  .=TRUE '&' ('not' Pj(c,z) 'or' Pj(c,z)) by BINARITH:18
  .=TRUE '&' TRUE by BINARITH:18
  .=TRUE by MARGREL1:45;
    hence thesis;
    end;
    hence thesis;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) '<' (a 'imp' c) 'eqv' (b 'imp' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume A1:Pj(a 'eqv' b,z)=TRUE;
      Pj(a 'eqv' b,z)
   =Pj((a 'imp' b) '&' (b 'imp' a),z) by BVFUNC_4:7
  .=Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z) by VALUAT_1:def 6;
then A2:Pj(a 'imp' b,z)=TRUE & Pj(b 'imp' a,z)=TRUE by A1,MARGREL1:45;
    then A3:'not' Pj(a,z) 'or' Pj(b,z) = TRUE by BVFUNC_1:def 11;
    A4: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
    A5: Pj(b 'imp' a,z) = 'not' Pj(b,z) 'or' Pj(a,z) by BVFUNC_1:def 11;
    A6:'not' Pj(b,z) 'or' Pj(a,z) = TRUE by A2,BVFUNC_1:def 11;
      Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
then A7:'not' Pj(b,z)=TRUE or Pj(a,z)=TRUE by A2,A5,BINARITH:7;
A8:Pj((a 'imp' c) 'eqv' (b 'imp' c),z)
   =Pj(((a 'imp' c) 'imp' (b 'imp' c)) '&' ((b 'imp' c) 'imp' (a 'imp' c)),z)
   by BVFUNC_4:7
  .=Pj((a 'imp' c) 'imp' (b 'imp' c),z) '&'
    Pj((b 'imp' c) 'imp' (a 'imp' c),z)
   by VALUAT_1:def 6
  .=('not' Pj(a 'imp' c,z) 'or' Pj(b 'imp' c,z)) '&'
    Pj((b 'imp' c) 'imp' (a 'imp' c),z)
   by BVFUNC_1:def 11
  .=('not' Pj(a 'imp' c,z) 'or' Pj(b 'imp' c,z)) '&'
    ('not' Pj(b 'imp' c,z) 'or' Pj(a 'imp' c,z))
   by BVFUNC_1:def 11
  .=('not'( 'not' Pj(a,z) 'or' Pj(c,z)) 'or' Pj(b 'imp' c,z)) '&'
    ('not' Pj(b 'imp' c,z) 'or' Pj(a 'imp' c,z))
   by BVFUNC_1:def 11
  .=('not'( 'not' Pj(a,z) 'or' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&'
    ('not' Pj(b 'imp' c,z) 'or' Pj(a 'imp' c,z))
   by BVFUNC_1:def 11
  .=('not'( 'not' Pj(a,z) 'or' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&'
    ('not'( 'not' Pj(b,z) 'or' Pj(c,z)) 'or' Pj(a 'imp' c,z))
   by BVFUNC_1:def 11
  .=('not'( 'not' Pj(a,z) 'or' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&'
    ('not'( 'not' Pj(b,z) 'or' Pj(c,z)) 'or' ('not' Pj(a,z) 'or' Pj(c,z)))
   by BVFUNC_1:def 11
  .=(('not' 'not' Pj(a,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(b,z)
  'or' Pj(c,z))) '&'
    ('not'( 'not' Pj(b,z) 'or' Pj(c,z)) 'or' ('not' Pj(a,z) 'or' Pj(c,z)))
   by BINARITH:10
  .=(('not' 'not' Pj(a,z) '&' 'not' Pj(c,z)) 'or' ('not'
Pj(b,z) 'or' Pj(c,z))) '&'
    (('not' 'not' Pj(b,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(a,z) 'or' Pj(c,z)))
   by BINARITH:10
  .=((Pj(a,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&'
    (('not' 'not' Pj(b,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(a,z) 'or' Pj(c,z)))
   by MARGREL1:40
  .=((Pj(a,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(b,z) 'or' Pj(c,z))) '&'
    ((Pj(b,z) '&' 'not' Pj(c,z)) 'or' ('not' Pj(a,z) 'or' Pj(c,z)))
   by MARGREL1:40;
     now per cases by A3,A4,BINARITH:7;
   case A9:'not' Pj(a,z)=TRUE;
     then A10:Pj(a,z)=FALSE by MARGREL1:41;
     then 'not' Pj(b,z)=TRUE by A6,BINARITH:7;
     then Pj(b,z)=FALSE by MARGREL1:41;
     then Pj((a 'imp' c) 'eqv' (b 'imp' c),z)
    =(FALSE 'or' (TRUE 'or' Pj(c,z))) '&'
     ((FALSE '&' 'not'
Pj(c,z)) 'or' (TRUE 'or' Pj(c,z))) by A8,A9,A10,MARGREL1:49
   .=(FALSE 'or' (TRUE 'or' Pj(c,z))) '&'
     (FALSE 'or' (TRUE 'or' Pj(c,z))) by MARGREL1:49
   .=(TRUE 'or' Pj(c,z)) '&' (FALSE 'or' (TRUE 'or' Pj(c,z))) by BINARITH:7
   .=(TRUE 'or' Pj(c,z)) '&' (TRUE 'or' Pj(c,z)) by BINARITH:7
   .=TRUE '&' (TRUE 'or' Pj(c,z)) by BINARITH:19
   .=TRUE '&' TRUE by BINARITH:19
   .=TRUE by MARGREL1:45;
     hence thesis;
   case A11:Pj(b,z)=TRUE;
     then 'not' Pj(b,z)=FALSE by MARGREL1:41;
     then Pj((a 'imp' c) 'eqv' (b 'imp' c),z)
    =('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) '&'
     ((TRUE '&' 'not' Pj(c,z)) 'or' (FALSE 'or' Pj(c,z)))
    by A7,A8,A11,MARGREL1:43,50
   .=('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) '&'
     ('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z)))
    by MARGREL1:50
   .=('not' Pj(c,z) 'or' Pj(c,z)) '&'
     ('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z)))
    by BINARITH:7
   .=('not' Pj(c,z) 'or' Pj(c,z)) '&' ('not' Pj(c,z) 'or' Pj(c,z))
    by BINARITH:7
   .=TRUE '&' ('not' Pj(c,z) 'or' Pj(c,z)) by BINARITH:18
   .=TRUE '&' TRUE by BINARITH:18
   .=TRUE by MARGREL1:45;
    hence thesis;
    end;
    hence thesis;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) '<' (c 'imp' a) 'eqv' (c 'imp' b)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume A1:Pj(a 'eqv' b,z)=TRUE;
      Pj(a 'eqv' b,z)
   =Pj((a 'imp' b) '&' (b 'imp' a),z) by BVFUNC_4:7
  .=Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z) by VALUAT_1:def 6;
then A2:Pj(a 'imp' b,z)=TRUE & Pj(b 'imp' a,z)=TRUE by A1,MARGREL1:45;
    then A3:'not' Pj(a,z) 'or' Pj(b,z) = TRUE by BVFUNC_1:def 11;
    A4: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
    A5: Pj(b 'imp' a,z) = 'not' Pj(b,z) 'or' Pj(a,z) by BVFUNC_1:def 11;
    A6:'not' Pj(b,z) 'or' Pj(a,z) = TRUE by A2,BVFUNC_1:def 11;
      Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
then A7:'not' Pj(b,z)=TRUE or Pj(a,z)=TRUE by A2,A5,BINARITH:7;
A8:Pj((c 'imp' a) 'eqv' (c 'imp' b),z)
   =Pj(((c 'imp' a) 'imp' (c 'imp' b)) '&' ((c 'imp' b) 'imp' (c 'imp' a)),z)
   by BVFUNC_4:7
  .=Pj((c 'imp' a) 'imp' (c 'imp' b),z) '&'
    Pj((c 'imp' b) 'imp' (c 'imp' a),z)
   by VALUAT_1:def 6
  .=('not' Pj(c 'imp' a,z) 'or' Pj(c 'imp' b,z)) '&'
    Pj((c 'imp' b) 'imp' (c 'imp' a),z)
   by BVFUNC_1:def 11
  .=('not' Pj(c 'imp' a,z) 'or' Pj(c 'imp' b,z)) '&'
    ('not' Pj(c 'imp' b,z) 'or' Pj(c 'imp' a,z))
   by BVFUNC_1:def 11
  .=('not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' Pj(c 'imp' b,z)) '&'
    ('not' Pj(c 'imp' b,z) 'or' Pj(c 'imp' a,z))
   by BVFUNC_1:def 11
  .=('not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&'
    ('not' Pj(c 'imp' b,z) 'or' Pj(c 'imp' a,z))
   by BVFUNC_1:def 11
  .=('not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&'
    ('not'( 'not' Pj(c,z) 'or' Pj(b,z)) 'or' Pj(c 'imp' a,z))
   by BVFUNC_1:def 11
  .=('not'( 'not' Pj(c,z) 'or' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&'
    ('not'( 'not' Pj(c,z) 'or' Pj(b,z)) 'or' ('not' Pj(c,z) 'or' Pj(a,z)))
   by BVFUNC_1:def 11
  .=(('not' 'not' Pj(c,z) '&' 'not' Pj(a,z)) 'or' ('not'
Pj(c,z) 'or' Pj(b,z))) '&'
    ('not'( 'not' Pj(c,z) 'or' Pj(b,z)) 'or' ('not' Pj(c,z) 'or' Pj(a,z)))
   by BINARITH:10
  .=(('not' 'not' Pj(c,z) '&' 'not' Pj(a,z)) 'or' ('not'
Pj(c,z) 'or' Pj(b,z))) '&'
    (('not' 'not' Pj(c,z) '&' 'not' Pj(b,z)) 'or' ('not' Pj(c,z) 'or' Pj(a,z)))
   by BINARITH:10
  .=((Pj(c,z) '&' 'not' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&'
    (('not' 'not' Pj(c,z) '&' 'not' Pj(b,z)) 'or' ('not' Pj(c,z) 'or' Pj(a,z)))
   by MARGREL1:40
  .=((Pj(c,z) '&' 'not' Pj(a,z)) 'or' ('not' Pj(c,z) 'or' Pj(b,z))) '&'
    ((Pj(c,z) '&' 'not' Pj(b,z)) 'or' ('not' Pj(c,z) 'or' Pj(a,z)))
   by MARGREL1:40;
     now per cases by A3,A4,BINARITH:7;
   case A9:'not' Pj(a,z)=TRUE;
     then A10:Pj(a,z)=FALSE by MARGREL1:41;
     then 'not' Pj(b,z)=TRUE by A6,BINARITH:7;
     then Pj(b,z)=FALSE by MARGREL1:41;
     then Pj((c 'imp' a) 'eqv' (c 'imp' b),z)
    =(Pj(c,z) 'or' ('not' Pj(c,z) 'or' FALSE)) '&'
     ((TRUE '&' Pj(c,z)) 'or' ('not' Pj(c,z) 'or' FALSE))
    by A8,A9,A10,MARGREL1:50
   .=(Pj(c,z) 'or' ('not' Pj(c,z) 'or' FALSE)) '&'
     (Pj(c,z) 'or' ('not' Pj(c,z) 'or' FALSE))
    by MARGREL1:50
   .=(Pj(c,z) 'or' 'not' Pj(c,z)) '&'
     (Pj(c,z) 'or' ('not' Pj(c,z) 'or' FALSE))
    by BINARITH:7
   .=(Pj(c,z) 'or' 'not' Pj(c,z)) '&' (Pj(c,z) 'or' 'not' Pj(c,z))
    by BINARITH:7
   .=TRUE '&' (Pj(c,z) 'or' 'not' Pj(c,z))
    by BINARITH:18
   .=TRUE '&' TRUE by BINARITH:18
   .=TRUE by MARGREL1:45;
     hence thesis;
   case A11:Pj(b,z)=TRUE;
     then 'not' Pj(b,z)=FALSE by MARGREL1:41;
     then Pj((c 'imp' a) 'eqv' (c 'imp' b),z)
    =(FALSE 'or' ('not' Pj(c,z) 'or' TRUE)) '&'
     ((FALSE '&' Pj(c,z)) 'or' ('not' Pj(c,z) 'or' TRUE))
    by A7,A8,A11,MARGREL1:43,49
   .=(FALSE 'or' ('not' Pj(c,z) 'or' TRUE)) '&'
     (FALSE 'or' ('not' Pj(c,z) 'or' TRUE))
    by MARGREL1:49
   .=('not' Pj(c,z) 'or' TRUE) '&'
     (FALSE 'or' ('not' Pj(c,z) 'or' TRUE))
    by BINARITH:7
   .=('not' Pj(c,z) 'or' TRUE) '&' ('not' Pj(c,z) 'or' TRUE)
    by BINARITH:7
   .=TRUE '&' ('not' Pj(c,z) 'or' TRUE)
    by BINARITH:19
   .=TRUE '&' TRUE by BINARITH:19
   .=TRUE by MARGREL1:45;
    hence thesis;
    end;
    hence thesis;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) '<' (a '&' c) 'eqv' (b '&' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume A1:Pj(a 'eqv' b,z)=TRUE;
      Pj(a 'eqv' b,z)
   =Pj((a 'imp' b) '&' (b 'imp' a),z) by BVFUNC_4:7
  .=Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z) by VALUAT_1:def 6;
then A2:Pj(a 'imp' b,z)=TRUE & Pj(b 'imp' a,z)=TRUE by A1,MARGREL1:45;
    then A3:'not' Pj(a,z) 'or' Pj(b,z) = TRUE by BVFUNC_1:def 11;
    A4: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
    A5: Pj(b 'imp' a,z) = 'not' Pj(b,z) 'or' Pj(a,z) by BVFUNC_1:def 11;
    A6:'not' Pj(b,z) 'or' Pj(a,z) = TRUE by A2,BVFUNC_1:def 11;
      Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
then A7:'not' Pj(b,z)=TRUE or Pj(a,z)=TRUE by A2,A5,BINARITH:7;
A8:Pj((a '&' c) 'eqv' (b '&' c),z)
   =Pj(((a '&' c) 'imp' (b '&' c)) '&' ((b '&' c) 'imp' (a '&' c)),z)
   by BVFUNC_4:7
  .=Pj((a '&' c) 'imp' (b '&' c),z) '&'
    Pj((b '&' c) 'imp' (a '&' c),z)
   by VALUAT_1:def 6
  .=('not' Pj(a '&' c,z) 'or' Pj(b '&' c,z)) '&'
    Pj((b '&' c) 'imp' (a '&' c),z)
   by BVFUNC_1:def 11
  .=('not' Pj(a '&' c,z) 'or' Pj(b '&' c,z)) '&'
    ('not' Pj(b '&' c,z) 'or' Pj(a '&' c,z))
   by BVFUNC_1:def 11
  .=('not'( Pj(a,z) '&' Pj(c,z)) 'or' Pj(b '&' c,z)) '&'
    ('not' Pj(b '&' c,z) 'or' Pj(a '&' c,z))
   by VALUAT_1:def 6
  .=('not'( Pj(a,z) '&' Pj(c,z)) 'or' (Pj(b,z) '&' Pj(c,z))) '&'
    ('not' Pj(b '&' c,z) 'or' Pj(a '&' c,z))
   by VALUAT_1:def 6
  .=('not'( Pj(a,z) '&' Pj(c,z)) 'or' (Pj(b,z) '&' Pj(c,z))) '&'
    ('not'( Pj(b,z) '&' Pj(c,z)) 'or' Pj(a '&' c,z))
   by VALUAT_1:def 6
  .=('not'( Pj(a,z) '&' Pj(c,z)) 'or' (Pj(b,z) '&' Pj(c,z))) '&'
    ('not'( Pj(b,z) '&' Pj(c,z)) 'or' (Pj(a,z) '&' Pj(c,z)))
   by VALUAT_1:def 6
  .=(('not' Pj(a,z) 'or' 'not' Pj(c,z)) 'or' (Pj(b,z) '&' Pj(c,z))) '&'
    ('not'( Pj(b,z) '&' Pj(c,z)) 'or' (Pj(a,z) '&' Pj(c,z)))
   by BINARITH:9
  .=(('not' Pj(a,z) 'or' 'not' Pj(c,z)) 'or' (Pj(b,z) '&' Pj(c,z))) '&'
    (('not' Pj(b,z) 'or' 'not' Pj(c,z)) 'or' (Pj(a,z) '&' Pj(c,z)))
   by BINARITH:9;
     now per cases by A3,A4,BINARITH:7;
   case A9:'not' Pj(a,z)=TRUE;
     then A10:Pj(a,z)=FALSE by MARGREL1:41;
     then 'not' Pj(b,z)=TRUE by A6,BINARITH:7;
     then Pj(b,z)=FALSE by MARGREL1:41;
     then Pj((a '&' c) 'eqv' (b '&' c),z)
    =((TRUE 'or' 'not' Pj(c,z)) 'or' FALSE) '&'
     ((TRUE 'or' 'not' Pj(c,z)) 'or' (FALSE '&' Pj(c,z)))
    by A8,A9,A10,MARGREL1:49
   .=((TRUE 'or' 'not' Pj(c,z)) 'or' FALSE) '&'
     ((TRUE 'or' 'not' Pj(c,z)) 'or' FALSE)
    by MARGREL1:49
   .=(TRUE 'or' 'not' Pj(c,z)) '&' ((TRUE 'or' 'not'
Pj(c,z)) 'or' FALSE) by BINARITH:7
   .=(TRUE 'or' 'not' Pj(c,z)) '&' (TRUE 'or' 'not' Pj(c,z)) by BINARITH:7
   .=TRUE '&' (TRUE 'or' 'not' Pj(c,z)) by BINARITH:19
   .=TRUE '&' TRUE by BINARITH:19
   .=TRUE by MARGREL1:45;
    hence thesis;
   case A11:Pj(b,z)=TRUE;
     then 'not' Pj(b,z)=FALSE by MARGREL1:41;
     then Pj((a '&' c) 'eqv' (b '&' c),z)
    =((FALSE 'or' 'not' Pj(c,z)) 'or' Pj(c,z)) '&'
     ((FALSE 'or' 'not'
Pj(c,z)) 'or' (TRUE '&' Pj(c,z))) by A7,A8,A11,MARGREL1:43,50
   .=((FALSE 'or' 'not' Pj(c,z)) 'or' Pj(c,z)) '&'
     ((FALSE 'or' 'not' Pj(c,z)) 'or' Pj(c,z)) by MARGREL1:50
   .=('not' Pj(c,z) 'or' Pj(c,z)) '&'
     ((FALSE 'or' 'not' Pj(c,z)) 'or' Pj(c,z)) by BINARITH:7
   .=('not' Pj(c,z) 'or' Pj(c,z)) '&' ('not' Pj(c,z) 'or' Pj(c,z))
   by BINARITH:7
   .=TRUE '&' ('not' Pj(c,z) 'or' Pj(c,z)) by BINARITH:18
   .=TRUE '&' TRUE by BINARITH:18
   .=TRUE by MARGREL1:45;
    hence thesis;
   end;
   hence thesis;
end;

theorem for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) '<' (a 'or' c) 'eqv' (b 'or' c)
proof
  let a,b,c be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume A1:Pj(a 'eqv' b,z)=TRUE;
      Pj(a 'eqv' b,z)
   =Pj((a 'imp' b) '&' (b 'imp' a),z) by BVFUNC_4:7
  .=Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z) by VALUAT_1:def 6;
then A2:Pj(a 'imp' b,z)=TRUE & Pj(b 'imp' a,z)=TRUE by A1,MARGREL1:45;
    then A3:'not' Pj(a,z) 'or' Pj(b,z) = TRUE by BVFUNC_1:def 11;
    A4: Pj(b,z)=TRUE or Pj(b,z)=FALSE by MARGREL1:39;
    A5: Pj(b 'imp' a,z) = 'not' Pj(b,z) 'or' Pj(a,z) by BVFUNC_1:def 11;
    A6:'not' Pj(b,z) 'or' Pj(a,z) = TRUE by A2,BVFUNC_1:def 11;
      Pj(a,z)=TRUE or Pj(a,z)=FALSE by MARGREL1:39;
then A7:'not' Pj(b,z)=TRUE or Pj(a,z)=TRUE by A2,A5,BINARITH:7;
A8:Pj((a 'or' c) 'eqv' (b 'or' c),z)
   =Pj(((a 'or' c) 'imp' (b 'or' c)) '&' ((b 'or' c) 'imp' (a 'or' c)),z)
   by BVFUNC_4:7
  .=Pj((a 'or' c) 'imp' (b 'or' c),z) '&'
    Pj((b 'or' c) 'imp' (a 'or' c),z)
   by VALUAT_1:def 6
  .=('not' Pj(a 'or' c,z) 'or' Pj(b 'or' c,z)) '&'
    Pj((b 'or' c) 'imp' (a 'or' c),z)
   by BVFUNC_1:def 11
  .=('not' Pj(a 'or' c,z) 'or' Pj(b 'or' c,z)) '&'
    ('not' Pj(b 'or' c,z) 'or' Pj(a 'or' c,z))
   by BVFUNC_1:def 11
  .=('not'( Pj(a,z) 'or' Pj(c,z)) 'or' Pj(b 'or' c,z)) '&'
    ('not' Pj(b 'or' c,z) 'or' Pj(a 'or' c,z))
   by BVFUNC_1:def 7
  .=('not'( Pj(a,z) 'or' Pj(c,z)) 'or' (Pj(b,z) 'or' Pj(c,z))) '&'
    ('not' Pj(b 'or' c,z) 'or' Pj(a 'or' c,z))
   by BVFUNC_1:def 7
  .=('not'( Pj(a,z) 'or' Pj(c,z)) 'or' (Pj(b,z) 'or' Pj(c,z))) '&'
    ('not'( Pj(b,z) 'or' Pj(c,z)) 'or' Pj(a 'or' c,z))
   by BVFUNC_1:def 7
  .=('not'( Pj(a,z) 'or' Pj(c,z)) 'or' (Pj(b,z) 'or' Pj(c,z))) '&'
    ('not'( Pj(b,z) 'or' Pj(c,z)) 'or' (Pj(a,z) 'or' Pj(c,z)))
   by BVFUNC_1:def 7
  .=(('not' Pj(a,z) '&' 'not' Pj(c,z)) 'or' (Pj(b,z) 'or' Pj(c,z))) '&'
    ('not'( Pj(b,z) 'or' Pj(c,z)) 'or' (Pj(a,z) 'or' Pj(c,z)))
   by BINARITH:10
  .=(('not' Pj(a,z) '&' 'not' Pj(c,z)) 'or' (Pj(b,z) 'or' Pj(c,z))) '&'
    (('not' Pj(b,z) '&' 'not' Pj(c,z)) 'or' (Pj(a,z) 'or' Pj(c,z)))
   by BINARITH:10;
     now per cases by A3,A4,BINARITH:7;
   case A9:'not' Pj(a,z)=TRUE;
     then A10:Pj(a,z)=FALSE by MARGREL1:41;
     then 'not' Pj(b,z)=TRUE by A6,BINARITH:7;
     then Pj(b,z)=FALSE by MARGREL1:41;
     then Pj((a 'or' c) 'eqv' (b 'or' c),z)
    =('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) '&'
     ((TRUE '&' 'not' Pj(c,z)) 'or' (FALSE 'or' Pj(c,z)))
    by A8,A9,A10,MARGREL1:50
   .=('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z))) '&'
     ('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z)))
    by MARGREL1:50
   .=('not' Pj(c,z) 'or' Pj(c,z)) '&'
     ('not' Pj(c,z) 'or' (FALSE 'or' Pj(c,z)))
    by BINARITH:7
   .=('not' Pj(c,z) 'or' Pj(c,z)) '&' ('not' Pj(c,z) 'or' Pj(c,z))
    by BINARITH:7
   .=TRUE '&' ('not' Pj(c,z) 'or' Pj(c,z))
    by BINARITH:18
   .=TRUE '&' TRUE
    by BINARITH:18
   .=TRUE by MARGREL1:45;
    hence thesis;
   case A11:Pj(b,z)=TRUE;
     then 'not' Pj(b,z)=FALSE by MARGREL1:41;
     then Pj((a 'or' c) 'eqv' (b 'or' c),z)
    =(FALSE 'or' (TRUE 'or' Pj(c,z))) '&'
     ((FALSE '&' 'not' Pj(c,z)) 'or' (TRUE 'or' Pj(c,z)))
    by A7,A8,A11,MARGREL1:43,49
   .=(FALSE 'or' (TRUE 'or' Pj(c,z))) '&'
     (FALSE 'or' (TRUE 'or' Pj(c,z)))
    by MARGREL1:49
   .=(TRUE 'or' Pj(c,z)) '&'
     (FALSE 'or' (TRUE 'or' Pj(c,z)))
    by BINARITH:7
   .=(TRUE 'or' Pj(c,z)) '&' (TRUE 'or' Pj(c,z))
    by BINARITH:7
   .=TRUE '&' (TRUE 'or' Pj(c,z))
    by BINARITH:19
   .=TRUE '&' TRUE by BINARITH:19
   .=TRUE by MARGREL1:45;
    hence thesis;
   end;
   hence thesis;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a '<' (a 'eqv' b) 'eqv' (b 'eqv' a) 'eqv' a
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume A1:Pj(a,z)=TRUE;
    then A2:'not' Pj(a,z)=FALSE by MARGREL1:41;
    A3:Pj('not' a,z)='not' Pj(a,z) by VALUAT_1:def 5;
A4:Pj((a 'eqv' b) 'eqv' (b 'eqv' a),z)
   =Pj(((a 'eqv' b) 'imp' (b 'eqv' a)) '&'
         ((b 'eqv' a) 'imp' (a 'eqv' b)),z)
    by BVFUNC_4:7
  .=Pj((a 'eqv' b) 'imp' (b 'eqv' a),z) '&'
    Pj((b 'eqv' a) 'imp' (a 'eqv' b),z)
    by VALUAT_1:def 6
  .=Pj('not'( a 'eqv' b) 'or' (b 'eqv' a),z) '&'
    Pj((b 'eqv' a) 'imp' (a 'eqv' b),z)
    by BVFUNC_4:8
  .=Pj('not'( a 'eqv' b) 'or' (b 'eqv' a),z) '&'
    Pj('not'( b 'eqv' a) 'or' (a 'eqv' b),z)
    by BVFUNC_4:8
  .=(Pj('not'( a 'eqv' b),z) 'or' Pj(b 'eqv' a,z)) '&'
    Pj('not'( b 'eqv' a) 'or' (a 'eqv' b),z)
    by BVFUNC_1:def 7
  .=(Pj('not'( a 'eqv' b),z) 'or' Pj(b 'eqv' a,z)) '&'
    (Pj('not'( b 'eqv' a),z) 'or' Pj(a 'eqv' b,z))
    by BVFUNC_1:def 7
  .=(Pj('not'( (a 'imp' b) '&' (b 'imp' a)),z) 'or' Pj(b 'eqv' a,z)) '&'
    (Pj('not'( b 'eqv' a),z) 'or' Pj(a 'eqv' b,z))
    by BVFUNC_4:7
  .=(Pj('not'( (a 'imp' b) '&' (b 'imp' a)),z) 'or' Pj(b 'eqv' a,z)) '&'
    (Pj('not'( b 'eqv' a),z) 'or' Pj((a 'imp' b) '&' (b 'imp' a),z))
    by BVFUNC_4:7
  .=(Pj('not'( (a 'imp' b) '&' (b 'imp' a)),z) 'or'
     Pj((b 'imp' a) '&' (a 'imp' b),z)) '&'
    (Pj('not'( b 'eqv' a),z) 'or' Pj((a 'imp' b) '&' (b 'imp' a),z))
    by BVFUNC_4:7
  .=(Pj('not'( (a 'imp' b) '&' (b 'imp' a)),z) 'or'
     Pj((b 'imp' a) '&' (a 'imp' b),z)) '&'
    (Pj('not'( (b 'imp' a) '&' (a 'imp' b)),z) 'or'
     Pj((a 'imp' b) '&' (b 'imp' a),z))
    by BVFUNC_4:7
  .=('not' Pj((a 'imp' b) '&' (b 'imp' a),z) 'or'
      Pj((b 'imp' a) '&' (a 'imp' b),z)) '&'
    (Pj('not'( (b 'imp' a) '&' (a 'imp' b)),z) 'or'
     Pj((a 'imp' b) '&' (b 'imp' a),z))
    by VALUAT_1:def 5
  .=('not' Pj((a 'imp' b) '&' (b 'imp' a),z) 'or'
      Pj((b 'imp' a) '&' (a 'imp' b),z)) '&'
    ('not' Pj((b 'imp' a) '&' (a 'imp' b),z) 'or'
      Pj((a 'imp' b) '&' (b 'imp' a),z))
    by VALUAT_1:def 5
  .=('not'( Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)) 'or'
      Pj((b 'imp' a) '&' (a 'imp' b),z)) '&'
    ('not' Pj((b 'imp' a) '&' (a 'imp' b),z) 'or'
      Pj((a 'imp' b) '&' (b 'imp' a),z))
    by VALUAT_1:def 6
  .=('not'( Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)) 'or'
      (Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z))) '&'
    ('not' Pj((b 'imp' a) '&' (a 'imp' b),z) 'or'
      Pj((a 'imp' b) '&' (b 'imp' a),z))
    by VALUAT_1:def 6
  .=('not'( Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)) 'or'
      (Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z))) '&'
    ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or'
      Pj((a 'imp' b) '&' (b 'imp' a),z))
    by VALUAT_1:def 6
  .=('not'( Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)) 'or'
      (Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z))) '&'
    ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or'
      (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)))
    by VALUAT_1:def 6
  .=('not'( Pj('not' a 'or' b,z) '&' Pj(b 'imp' a,z)) 'or'
      (Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z))) '&'
    ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or'
      (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)))
    by BVFUNC_4:8
  .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or'
      (Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z))) '&'
    ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or'
      (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)))
    by BVFUNC_4:8
  .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or'
      (Pj('not' b 'or' a,z) '&' Pj(a 'imp' b,z))) '&'
    ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or'
      (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)))
    by BVFUNC_4:8
  .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or'
      (Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z))) '&'
    ('not'( Pj(b 'imp' a,z) '&' Pj(a 'imp' b,z)) 'or'
      (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)))
    by BVFUNC_4:8
  .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or'
      (Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z))) '&'
    ('not'( Pj('not' b 'or' a,z) '&' Pj(a 'imp' b,z)) 'or'
      (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)))
    by BVFUNC_4:8
  .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or'
      (Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z))) '&'
    ('not'( Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z)) 'or'
      (Pj(a 'imp' b,z) '&' Pj(b 'imp' a,z)))
    by BVFUNC_4:8
  .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or'
      (Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z))) '&'
    ('not'( Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z)) 'or'
      (Pj('not' a 'or' b,z) '&' Pj(b 'imp' a,z)))
    by BVFUNC_4:8
  .=('not'( Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)) 'or'
      (Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z))) '&'
    ('not'( Pj('not' b 'or' a,z) '&' Pj('not' a 'or' b,z)) 'or'
      (Pj('not' a 'or' b,z) '&' Pj('not' b 'or' a,z)))
    by BVFUNC_4:8
  .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b 'or' a,z))) 'or'
      ((Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z)))) '&'
    ('not'( (Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z))) 'or'
      ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z))))
    by BVFUNC_1:def 7
  .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or'
      ((Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z)))) '&'
    ('not'( (Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z))) 'or'
      ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z))))
    by BVFUNC_1:def 7
  .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or'
      ((Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a 'or' b,z)))) '&'
    ('not'( (Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z))) 'or'
      ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z))))
    by BVFUNC_1:def 7
  .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or'
      ((Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z)))) '&'
    ('not'( (Pj('not' b 'or' a,z)) '&' (Pj('not' a 'or' b,z))) 'or'
      ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z))))
    by BVFUNC_1:def 7
  .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or'
      ((Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z)))) '&'
    ('not'( (Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a 'or' b,z))) 'or'
      ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z))))
    by BVFUNC_1:def 7
  .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or'
      ((Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z)))) '&'
    ('not'( (Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z))) 'or'
      ((Pj('not' a 'or' b,z)) '&' (Pj('not' b 'or' a,z))))
    by BVFUNC_1:def 7
  .=('not'( (Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' Pj(a,z))) 'or'
      ((Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z)))) '&'
    ('not'( (Pj('not' b,z) 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' Pj(b,z))) 'or'
      ((Pj('not' a,z) 'or' Pj(b,z)) '&' (Pj('not' b 'or' a,z))))
    by BVFUNC_1:def 7
  .=('not'( (FALSE 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' TRUE)) 'or'
      ((Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z)))) '&'
    ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or'
      ((FALSE 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' TRUE)))
    by A1,A2,A3,BVFUNC_1:def 7
  .=('not'( Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE)) 'or'
      ((Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z)))) '&'
    ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or'
      ((FALSE 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' TRUE)))
    by BINARITH:7
  .=('not'( Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE)) 'or'
      ((Pj('not' b,z) 'or' TRUE) '&' Pj(b,z))) '&'
    ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or'
      ((FALSE 'or' Pj(b,z)) '&' (Pj('not' b,z) 'or' TRUE)))
    by BINARITH:7
  .=('not'( Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE)) 'or'
      ((Pj('not' b,z) 'or' TRUE) '&' Pj(b,z))) '&'
    ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or'
      (Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE)))
    by BINARITH:7
  .=('not'( Pj(b,z) '&' TRUE) 'or'
      ((Pj('not' b,z) 'or' TRUE) '&' Pj(b,z))) '&'
    ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or'
      (Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE)))
    by BINARITH:19
  .=('not'( Pj(b,z) '&' TRUE) 'or' (TRUE '&' Pj(b,z))) '&'
    ('not'( (Pj('not' b,z) 'or' TRUE) '&' (FALSE 'or' Pj(b,z))) 'or'
      (Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE)))
    by BINARITH:19
  .=('not'( Pj(b,z) '&' TRUE) 'or' (TRUE '&' Pj(b,z))) '&'
    ('not'( TRUE '&' (FALSE 'or' Pj(b,z))) 'or'
      (Pj(b,z) '&' (Pj('not' b,z) 'or' TRUE)))
    by BINARITH:19
  .=('not'( Pj(b,z) '&' TRUE) 'or' (TRUE '&' Pj(b,z))) '&'
    ('not'( TRUE '&' (FALSE 'or' Pj(b,z))) 'or'
      (Pj(b,z) '&' TRUE))
    by BINARITH:19
  .=('not'( TRUE '&' Pj(b,z)) 'or' (TRUE '&' Pj(b,z))) '&'
    ('not'( TRUE '&' Pj(b,z)) 'or' (Pj(b,z) '&' TRUE)) by BINARITH:7
  .=('not' Pj(b,z) 'or' (TRUE '&' Pj(b,z))) '&'
    ('not'( TRUE '&' Pj(b,z)) 'or' (TRUE '&' Pj(b,z)))
    by MARGREL1:50
  .=('not' Pj(b,z) 'or' (TRUE '&' Pj(b,z))) '&'
    ('not' Pj(b,z) 'or' (TRUE '&' Pj(b,z)))
    by MARGREL1:50
  .=('not' Pj(b,z) 'or' Pj(b,z)) '&'
    ('not' Pj(b,z) 'or' (TRUE '&' Pj(b,z)))
    by MARGREL1:50
  .=('not' Pj(b,z) 'or' Pj(b,z)) '&' ('not' Pj(b,z) 'or' Pj(b,z))
    by MARGREL1:50
  .=TRUE '&' ('not' Pj(b,z) 'or' Pj(b,z))
    by BINARITH:18
  .=TRUE '&' TRUE
    by BINARITH:18
  .=TRUE by MARGREL1:45;
      Pj((a 'eqv' b) 'eqv' (b 'eqv' a) 'eqv' a,z)
   =Pj((((a 'eqv' b) 'eqv' (b 'eqv' a)) 'imp' a) '&'
       (a 'imp' ((a 'eqv' b) 'eqv' (b 'eqv' a))),z)
    by BVFUNC_4:7
  .=Pj(((a 'eqv' b) 'eqv' (b 'eqv' a)) 'imp' a,z) '&'
       Pj(a 'imp' ((a 'eqv' b) 'eqv' (b 'eqv' a)),z)
    by VALUAT_1:def 6
  .=('not' Pj((a 'eqv' b) 'eqv' (b 'eqv' a),z) 'or' Pj(a,z)) '&'
       Pj(a 'imp' ((a 'eqv' b) 'eqv' (b 'eqv' a)),z)
    by BVFUNC_1:def 11
  .=('not' Pj((a 'eqv' b) 'eqv' (b 'eqv' a),z) 'or' Pj(a,z)) '&'
    ('not' Pj(a,z) 'or' Pj((a 'eqv' b) 'eqv' (b 'eqv' a),z))
    by BVFUNC_1:def 11
  .=(FALSE 'or' Pj(a,z)) '&' ('not' Pj(a,z) 'or' TRUE)
    by A4,MARGREL1:41
  .=Pj(a,z) '&' ('not' Pj(a,z) 'or' TRUE)
    by BINARITH:7
  .=TRUE '&' Pj(a,z) by BINARITH:19
  .=TRUE by A1,MARGREL1:50;
    hence thesis;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a '<' (a 'imp' b) 'eqv' b
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume A1:Pj(a,z)=TRUE;
    then A2:'not' Pj(a,z)=FALSE by MARGREL1:41;
      Pj((a 'imp' b) 'eqv' b,z)
   =Pj(('not' a 'or' b) 'eqv' b,z) by BVFUNC_4:8
  .=Pj((('not' a 'or' b) 'imp' b) '&' (b 'imp' ('not' a 'or' b)),z)
  by BVFUNC_4:7
  .=Pj(('not'( 'not' a 'or' b) 'or' b) '&' (b 'imp' ('not'
a 'or' b)),z) by BVFUNC_4:8
  .=Pj(('not'( 'not' a 'or' b) 'or' b) '&' ('not' b 'or' ('not'
a 'or' b)),z) by BVFUNC_4:8
  .=Pj('not'( 'not' a 'or' b) 'or' b,z) '&' Pj('not' b 'or' ('not' a 'or' b),z)
   by VALUAT_1:def 6
  .=(Pj('not'( 'not' a 'or' b),z) 'or' Pj(b,z)) '&' Pj('not' b 'or' ('not'
a 'or' b),z)
   by BVFUNC_1:def 7
  .=('not' Pj('not' a 'or' b,z) 'or' Pj(b,z)) '&' Pj('not' b 'or' ('not'
a 'or' b),z)
   by VALUAT_1:def 5
  .=('not'( Pj('not' a,z) 'or' Pj(b,z)) 'or' Pj(b,z)) '&'
  Pj('not' b 'or' ('not' a 'or' b),z)
   by BVFUNC_1:def 7
  .=('not'( 'not' Pj(a,z) 'or' Pj(b,z)) 'or' Pj(b,z)) '&'
  Pj('not' b 'or' ('not' a 'or' b),z)
   by VALUAT_1:def 5
  .=(('not' 'not' Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&'
  Pj('not' b 'or' ('not' a 'or' b),z)
   by BINARITH:10
  .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&' Pj('not' b 'or' ('not'
a 'or' b),z)
   by MARGREL1:40
  .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&'
  (Pj('not' b,z) 'or' Pj('not' a 'or' b,z))
   by BVFUNC_1:def 7
  .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&'
    (Pj('not' b,z) 'or' (Pj('not' a,z) 'or' Pj(b,z)))
   by BVFUNC_1:def 7
  .=((Pj(a,z) '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&'
    (Pj('not' b,z) 'or' ('not' Pj(a,z) 'or' Pj(b,z)))
   by VALUAT_1:def 5
  .=((TRUE '&' 'not' Pj(b,z)) 'or' Pj(b,z)) '&'
    ('not' Pj(b,z) 'or' (FALSE 'or' Pj(b,z)))
   by A1,A2,VALUAT_1:def 5
  .=('not' Pj(b,z) 'or' Pj(b,z)) '&'
    ('not' Pj(b,z) 'or' (FALSE 'or' Pj(b,z)))
   by MARGREL1:50
  .=('not' Pj(b,z) 'or' Pj(b,z)) '&'
    ('not' Pj(b,z) 'or' Pj(b,z))
   by BINARITH:7
  .=TRUE '&' ('not' Pj(b,z) 'or' Pj(b,z))
   by BINARITH:18
  .=TRUE '&' TRUE
   by BINARITH:18
  .=TRUE by MARGREL1:45;
    hence thesis;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a '<' (b 'imp' a) 'eqv' a
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume A1:Pj(a,z)=TRUE;
    then A2:'not' Pj(a,z)=FALSE by MARGREL1:41;
      Pj((b 'imp' a) 'eqv' a,z)
   =Pj(('not' b 'or' a) 'eqv' a,z) by BVFUNC_4:8
  .=Pj((('not' b 'or' a) 'imp' a) '&' (a 'imp' ('not' b 'or' a)),z)
  by BVFUNC_4:7
  .=Pj(('not'( 'not' b 'or' a) 'or' a) '&' (a 'imp' ('not'
b 'or' a)),z) by BVFUNC_4:8
  .=Pj(('not'( 'not' b 'or' a) 'or' a) '&' ('not' a 'or' ('not'
b 'or' a)),z) by BVFUNC_4:8
  .=Pj('not'( 'not' b 'or' a) 'or' a,z) '&' Pj('not' a 'or' ('not' b 'or' a),z)
   by VALUAT_1:def 6
  .=(Pj('not'( 'not' b 'or' a),z) 'or' Pj(a,z)) '&' Pj('not' a 'or' ('not'
b 'or' a),z)
   by BVFUNC_1:def 7
  .=('not' Pj('not' b 'or' a,z) 'or' Pj(a,z)) '&' Pj('not' a 'or' ('not'
b 'or' a),z) by VALUAT_1:def 5
  .=('not'( Pj('not' b,z) 'or' Pj(a,z)) 'or' Pj(a,z)) '&'
  Pj('not' a 'or' ('not' b 'or' a),z)
   by BVFUNC_1:def 7
  .=('not'( 'not' Pj(b,z) 'or' Pj(a,z)) 'or' Pj(a,z)) '&'
  Pj('not' a 'or' ('not' b 'or' a),z)
   by VALUAT_1:def 5
  .=(('not' 'not' Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&'
  Pj('not' a 'or' ('not' b 'or' a),z)
   by BINARITH:10
  .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&' Pj('not' a 'or' ('not'
b 'or' a),z)
   by MARGREL1:40
  .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&'
  (Pj('not' a,z) 'or' Pj('not' b 'or' a,z))
   by BVFUNC_1:def 7
  .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&'
    (Pj('not' a,z) 'or' (Pj('not' b,z) 'or' Pj(a,z)))
   by BVFUNC_1:def 7
  .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&'
    (Pj('not' a,z) 'or' ('not' Pj(b,z) 'or' Pj(a,z)))
   by VALUAT_1:def 5
  .=((Pj(b,z) '&' 'not' Pj(a,z)) 'or' Pj(a,z)) '&'
    ('not' Pj(a,z) 'or' ('not' Pj(b,z) 'or' Pj(a,z)))
   by VALUAT_1:def 5
  .=TRUE '&' (FALSE 'or' ('not' Pj(b,z) 'or' TRUE))
   by A1,A2,BINARITH:19
  .=FALSE 'or' ('not' Pj(b,z) 'or' TRUE)
   by MARGREL1:50
  .='not' Pj(b,z) 'or' TRUE
   by BINARITH:7
  .=TRUE by BINARITH:19;
    hence thesis;
end;

theorem for a,b being Element of Funcs(Y,BOOLEAN) holds
a '<' (a '&' b) 'eqv' (b '&' a) 'eqv' a
proof
  let a,b be Element of Funcs(Y,BOOLEAN);
    let z be Element of Y;
    assume A1:Pj(a,z)=TRUE;
A2:Pj((a '&' b) 'eqv' (a '&' b),z)
   =Pj(((a '&' b) 'imp' (a '&' b)) '&' ((a '&' b) 'imp' (a '&' b)),z)
   by BVFUNC_4:7
  .=Pj((a '&' b) 'imp' (a '&' b),z) '&' Pj((a '&' b) 'imp' (a '&' b),z)
   by VALUAT_1:def 6
  .=Pj((a '&' b) 'imp' (a '&' b),z)
   by BINARITH:16
  .=Pj('not'( a '&' b) 'or' (a '&' b),z)
   by BVFUNC_4:8
  .=Pj(I_el(Y),z) by BVFUNC_4:6
  .=TRUE by BVFUNC_1:def 14;
      Pj((a '&' b) 'eqv' (b '&' a) 'eqv' a,z)
   =Pj((((a '&' b) 'eqv' (a '&' b)) 'imp' a) '&'
       (a 'imp' ((a '&' b) 'eqv' (a '&' b))),z) by BVFUNC_4:7
  .=Pj(((a '&' b) 'eqv' (a '&' b)) 'imp' a,z) '&'
    Pj(a 'imp' ((a '&' b) 'eqv' (a '&' b)),z)
   by VALUAT_1:def 6
  .=Pj('not'( (a '&' b) 'eqv' (a '&' b)) 'or' a,z) '&'
    Pj(a 'imp' ((a '&' b) 'eqv' (a '&' b)),z)
   by BVFUNC_4:8
  .=Pj('not'( (a '&' b) 'eqv' (a '&' b)) 'or' a,z) '&'
    Pj('not' a 'or' ((a '&' b) 'eqv' (a '&' b)),z)
   by BVFUNC_4:8
  .=(Pj('not'( (a '&' b) 'eqv' (a '&' b)),z) 'or' Pj(a,z)) '&'
    Pj('not' a 'or' ((a '&' b) 'eqv' (a '&' b)),z)
   by BVFUNC_1:def 7
  .=(Pj('not'( (a '&' b) 'eqv' (a '&' b)),z) 'or' Pj(a,z)) '&'
    (Pj('not' a,z) 'or' Pj((a '&' b) 'eqv' (a '&' b),z))
   by BVFUNC_1:def 7
  .=('not' Pj((a '&' b) 'eqv' (a '&' b),z) 'or' Pj(a,z)) '&'
    (Pj('not' a,z) 'or' Pj((a '&' b) 'eqv' (a '&' b),z))
   by VALUAT_1:def 5
  .=(FALSE 'or' Pj(a,z)) '&' (Pj('not' a,z) 'or' TRUE)
   by A2,MARGREL1:41
  .=Pj(a,z) '&' (Pj('not' a,z) 'or' TRUE)
   by BINARITH:7
  .=TRUE '&' Pj(a,z) by BINARITH:19
  .=TRUE by A1,MARGREL1:50;
    hence thesis;
end;

Back to top