:: Predicate Calculus for Boolean Valued Functions, { I }
::  by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received December 21, 1998
:: Copyright (c) 1998-2018 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, SUBSET_1, PARTIT1, MARGREL1, EQREL_1, BVFUNC_1,
      BVFUNC_2, XBOOLEAN, FUNCT_1;
 notations XBOOLE_0, SUBSET_1, XBOOLEAN, MARGREL1, FUNCT_2, EQREL_1, BVFUNC_1,
      BVFUNC_2;
 constructors BVFUNC_1, BVFUNC_2, RELSET_1, NUMBERS;
 registrations MARGREL1, ORDINAL1;
 requirements BOOLE, NUMERALS;
 definitions BVFUNC_1;
 equalities XBOOLEAN;
 expansions BVFUNC_1;
 theorems MARGREL1, BINARITH, BVFUNC_1, BVFUNC_2, XBOOLEAN, EQREL_1;

begin :: Chap. 1  Predicate Calculus

reserve Y for non empty set,
  G for Subset of PARTITIONS(Y),
  a,b,c,u for Function of 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;
A1: ('not' a.z)=TRUE or ('not' a.z)=FALSE by XBOOLEAN:def 3;
A2: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
  assume (a 'imp' b).z=TRUE;
  then
A3: ('not' a.z) 'or' b.z=TRUE by BVFUNC_1:def 8;
  per cases by A3,A1,BINARITH:3;
  suppose
    'not' a.z=TRUE;
    then a.z=FALSE by MARGREL1:11;
    then B_INF(a,CompF(PA,G)).z = FALSE by A2,BVFUNC_1:def 16;
    then All(a,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' FALSE) 'or' Ex(b,PA,G).z by
BVFUNC_1:def 8
      .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11
      .=TRUE by BINARITH:10;
  end;
  suppose
    b.z=TRUE;
    then B_SUP(b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17;
    then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10;
    hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by
BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
end;

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

theorem
  (a '&' b) '<' (Ex(a,PA,G) '&' Ex(b,PA,G))
proof
  let z be Element of Y;
A1: (a '&' b).z=a.z '&' b.z by MARGREL1:def 20;
  assume
A2: (a '&' b).z=TRUE;
  then
A3: Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) & a.z=TRUE by A1,BVFUNC_2:def 10
,MARGREL1:12;
A4: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
  b.z=TRUE by A2,A1,MARGREL1:12;
  then B_SUP(b,CompF(PA,G)).z = TRUE by A4,BVFUNC_1:def 17;
  then
A5: Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10;
  thus (Ex(a,PA,G) '&' Ex(b,PA,G)).z =Ex(a,PA,G).z '&' Ex(b,PA,G).z by
MARGREL1:def 20
    .=TRUE '&' TRUE by A3,A4,A5,BVFUNC_1:def 17
    .=TRUE;
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(b,PA,G) = B_INF(b,CompF(PA,G)) by BVFUNC_2:def 9;
A2: All(a,PA,G) = B_INF(a,CompF(PA,G)) by BVFUNC_2:def 9;
A3: 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;
A4: (Ex('not' a,PA,G) 'or' Ex('not' b,PA,G)).z =Ex('not' a,PA,G).z 'or'
    Ex('not' b,PA,G).z by BVFUNC_1:def 4;
A5: Ex('not' b,PA,G).z=TRUE or Ex('not' b,PA,G).z=FALSE by XBOOLEAN:def 3;
    assume
A6: (Ex('not' a,PA,G) 'or' Ex('not' b,PA,G)).z=TRUE;
    per cases by A6,A4,A5,BINARITH:3;
    suppose
A7:   Ex('not' a,PA,G).z=TRUE;
      now
        assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
        ('not' a).x=TRUE);
        then B_SUP('not' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
        hence contradiction by A7,BVFUNC_2:def 10;
      end;
      then consider x1 being Element of Y such that
A8:   x1 in EqClass(z,CompF(PA,G)) and
A9:   ('not' a).x1=TRUE;
      'not' a.x1=TRUE by A9,MARGREL1:def 19;
      then
A10:  a.x1=FALSE by MARGREL1:11;
      thus ('not' (All(a,PA,G) '&' All(b,PA,G))).z ='not' ((All(a,PA,G) '&'
      All(b,PA,G))).z by MARGREL1:def 19
        .='not' (All(a,PA,G).z '&' All(b,PA,G).z) by MARGREL1:def 20
        .='not' (FALSE '&' All(b,PA,G).z) by A2,A8,A10,BVFUNC_1:def 16
        .='not' (FALSE) by MARGREL1:12
        .=TRUE by MARGREL1:11;
    end;
    suppose
A11:  Ex('not' b,PA,G).z=TRUE;
      now
        assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
        ('not' b).x=TRUE);
        then B_SUP('not' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
        hence contradiction by A11,BVFUNC_2:def 10;
      end;
      then consider x1 being Element of Y such that
A12:  x1 in EqClass(z,CompF(PA,G)) and
A13:  ('not' b).x1=TRUE;
      'not' b.x1=TRUE by A13,MARGREL1:def 19;
      then
A14:  b.x1=FALSE by MARGREL1:11;
      thus ('not' (All(a,PA,G) '&' All(b,PA,G))).z ='not' ((All(a,PA,G) '&'
      All(b,PA,G))).z by MARGREL1:def 19
        .='not' (All(a,PA,G).z '&' All(b,PA,G).z) by MARGREL1:def 20
        .='not' (All(a,PA,G).z '&' FALSE) by A1,A12,A14,BVFUNC_1:def 16
        .='not' (FALSE) by MARGREL1:12
        .=TRUE by MARGREL1:11;
    end;
  end;
  '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 ('not' (All(a,PA,G) '&' All(b,PA,G))).z=TRUE;
    then
A15: 'not' ((All(a,PA,G) '&' All(b,PA,G))).z=TRUE by MARGREL1:def 19;
    (All(a,PA,G) '&' All(b,PA,G)).z =All(a,PA,G).z '&' All(b,PA,G).z by
MARGREL1:def 20;
    then
A16: All(a,PA,G).z '&' All(b,PA,G).z=FALSE by A15,MARGREL1:11;
    per cases by A16,MARGREL1:12;
    suppose
      All(a,PA,G).z=FALSE;
      then consider x1 being Element of Y such that
A17:  x1 in EqClass(z,CompF(PA,G)) and
A18:  a.x1<>TRUE by A2,BVFUNC_1:def 16;
      a.x1=FALSE by A18,XBOOLEAN:def 3;
      then 'not' a.x1=TRUE by MARGREL1:11;
      then ('not' a).x1=TRUE by MARGREL1:def 19;
      then B_SUP('not' a,CompF(PA,G)).z = TRUE by A17,BVFUNC_1:def 17;
      then Ex('not' a,PA,G).z =TRUE by BVFUNC_2:def 10;
      hence
      (Ex('not' a,PA,G) 'or' Ex('not' b,PA,G)).z =TRUE 'or' Ex('not' b,PA
      ,G).z by BVFUNC_1:def 4
        .=TRUE by BINARITH:10;
    end;
    suppose
      All(b,PA,G).z=FALSE;
      then consider x1 being Element of Y such that
A19:  x1 in EqClass(z,CompF(PA,G)) and
A20:  b.x1<>TRUE by A1,BVFUNC_1:def 16;
      b.x1=FALSE by A20,XBOOLEAN:def 3;
      then 'not' b.x1=TRUE by MARGREL1:11;
      then ('not' b).x1=TRUE by MARGREL1:def 19;
      then B_SUP('not' b,CompF(PA,G)).z = TRUE by A19,BVFUNC_1:def 17;
      then Ex('not' b,PA,G).z =TRUE by BVFUNC_2:def 10;
      hence
      (Ex('not' a,PA,G) 'or' Ex('not' b,PA,G)).z =Ex('not' a,PA,G).z 'or'
      TRUE by BVFUNC_1:def 4
        .=TRUE by BINARITH:10;
    end;
  end;
  hence thesis by A3,BVFUNC_1:15;
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' b,PA,G) = B_INF('not' b,CompF(PA,G)) by BVFUNC_2:def 9;
A2: Ex(b,PA,G) = B_SUP(b,CompF(PA,G)) by BVFUNC_2:def 10;
A3: Ex(a,PA,G) = B_SUP(a,CompF(PA,G)) by BVFUNC_2:def 10;
A4: 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;
A5: All('not' b,PA,G).z=TRUE or All('not' b,PA,G).z=FALSE by XBOOLEAN:def 3;
    assume (All('not' a,PA,G) 'or' All('not' b,PA,G)) .z=TRUE;
    then
A6: All('not' a,PA,G).z 'or' All('not' b,PA,G).z=TRUE by BVFUNC_1:def 4;
    per cases by A6,A5,BINARITH:3;
    suppose
A7:   All('not' a,PA,G).z=TRUE;
A8:   now
        assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
        holds ('not' a).x=TRUE);
        then B_INF('not' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
        hence contradiction by A7,BVFUNC_2:def 9;
      end;
A9:   now
        let x be Element of Y;
        assume x in EqClass(z,CompF(PA,G));
        then ('not' a).x=TRUE by A8;
        then 'not' a.x=TRUE by MARGREL1:def 19;
        hence a.x<>TRUE by MARGREL1:11;
      end;
      thus ('not' (Ex(a,PA,G) '&' Ex(b,PA,G))).z ='not' (Ex(a,PA,G) '&' Ex(b,
      PA,G)).z by MARGREL1:def 19
        .='not' (Ex(a,PA,G).z '&' Ex(b,PA,G).z) by MARGREL1:def 20
        .='not' (FALSE '&' Ex(b,PA,G).z) by A3,A9,BVFUNC_1:def 17
        .='not' (FALSE) by MARGREL1:12
        .=TRUE by MARGREL1:11;
    end;
    suppose
A10:  All('not' b,PA,G).z=TRUE;
A11:  now
        assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
        holds ('not' b).x=TRUE);
        then B_INF('not' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
        hence contradiction by A10,BVFUNC_2:def 9;
      end;
A12:  now
        let x be Element of Y;
        assume x in EqClass(z,CompF(PA,G));
        then ('not' b).x=TRUE by A11;
        then 'not' b.x=TRUE by MARGREL1:def 19;
        hence b.x<>TRUE by MARGREL1:11;
      end;
      thus ('not' (Ex(a,PA,G) '&' Ex(b,PA,G))).z ='not' (Ex(a,PA,G) '&' Ex(b,
      PA,G)).z by MARGREL1:def 19
        .='not' (Ex(a,PA,G).z '&' Ex(b,PA,G).z) by MARGREL1:def 20
        .='not' (Ex(a,PA,G).z '&' FALSE) by A2,A12,BVFUNC_1:def 17
        .='not' (FALSE) by MARGREL1:12
        .=TRUE by MARGREL1:11;
    end;
  end;
A13: All('not' a,PA,G) = B_INF('not' a,CompF(PA,G)) by BVFUNC_2:def 9;
  '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 ('not' (Ex(a,PA,G) '&' Ex(b,PA,G))).z=TRUE;
    then 'not' (Ex(a,PA,G) '&' Ex(b,PA,G)).z=TRUE by MARGREL1:def 19;
    then (Ex(a,PA,G) '&' Ex(b,PA,G)).z=FALSE by MARGREL1:11;
    then
A14: Ex(a,PA,G).z '&' Ex(b,PA,G).z=FALSE by MARGREL1:def 20;
    per cases by A14,MARGREL1:12;
    suppose
A15:  Ex(a,PA,G).z=FALSE;
A16:  now
        let x be Element of Y;
        assume x in EqClass(z,CompF(PA,G));
        then a.x<>TRUE by A3,A15,BVFUNC_1:def 17;
        then a.x=FALSE by XBOOLEAN:def 3;
        then 'not' a.x=TRUE by MARGREL1:11;
        hence ('not' a).x=TRUE by MARGREL1:def 19;
      end;
      thus (All('not' a,PA,G) 'or' All('not' b,PA,G)) .z = All('not' a,PA,G).z
      'or' All('not' b,PA,G).z by BVFUNC_1:def 4
        .= TRUE 'or' All('not' b,PA,G).z by A13,A16,BVFUNC_1:def 16
        .= TRUE by BINARITH:10;
    end;
    suppose
A17:  Ex(b,PA,G).z=FALSE;
A18:  now
        let x be Element of Y;
        assume x in EqClass(z,CompF(PA,G));
        then b.x<>TRUE by A2,A17,BVFUNC_1:def 17;
        then b.x=FALSE by XBOOLEAN:def 3;
        then 'not' b.x=TRUE by MARGREL1:11;
        hence ('not' b).x=TRUE by MARGREL1:def 19;
      end;
      thus (All('not' a,PA,G) 'or' All('not' b,PA,G)) .z = All('not' a,PA,G).z
      'or' All('not' b,PA,G).z by BVFUNC_1:def 4
        .= All('not' a,PA,G).z 'or' TRUE by A1,A18,BVFUNC_1:def 16
        .= TRUE by BINARITH:10;
    end;
  end;
  hence thesis by A4,BVFUNC_1:15;
end;

theorem
  (All(a,PA,G) 'or' All(b,PA,G)) '<' (a 'or' b)
proof
  let z be Element of Y;
A1: All(a,PA,G).z=TRUE or All(a,PA,G).z=FALSE by XBOOLEAN:def 3;
A2: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
  assume (All(a,PA,G) 'or' All(b,PA,G)) .z=TRUE;
  then
A3: All(a,PA,G).z 'or' All(b,PA,G).z=TRUE by BVFUNC_1:def 4;
  per cases by A3,A1,BINARITH:3;
  suppose
A4: 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 a.x=TRUE);
      then B_INF(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
      hence contradiction by A4,BVFUNC_2:def 9;
    end;
    thus (a 'or' b).z = a.z 'or' b.z by BVFUNC_1:def 4
      .= TRUE 'or' b.z by A2,A5
      .= TRUE by BINARITH:10;
  end;
  suppose
A6: 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 b.x=TRUE);
      then B_INF(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
      hence contradiction by A6,BVFUNC_2:def 9;
    end;
    thus (a 'or' b).z = a.z 'or' b.z by BVFUNC_1:def 4
      .= a.z 'or' TRUE by A2,A7
      .= TRUE by BINARITH:10;
  end;
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;
  let z be Element of Y;
A2: Ex(b,PA,G) = B_SUP(b,CompF(PA,G)) by BVFUNC_2:def 10;
A3: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
  assume (a 'or' b).z=TRUE;
  then
A4: a.z 'or' b.z=TRUE by BVFUNC_1:def 4;
A5: b.z=TRUE or b.z=FALSE by XBOOLEAN:def 3;
  per cases by A4,A5,BINARITH:3;
  suppose
A6: a.z=TRUE;
    thus (Ex(a,PA,G) 'or' Ex(b,PA,G)).z =Ex(a,PA,G).z 'or' Ex(b,PA,G).z by
BVFUNC_1:def 4
      .=TRUE 'or' Ex(b,PA,G).z by A1,A3,A6,BVFUNC_1:def 17
      .=TRUE by BINARITH:10;
  end;
  suppose
A7: b.z=TRUE;
    thus (Ex(a,PA,G) 'or' Ex(b,PA,G)).z =Ex(a,PA,G).z 'or' Ex(b,PA,G).z by
BVFUNC_1:def 4
      .=Ex(a,PA,G).z 'or' TRUE by A2,A3,A7,BVFUNC_1:def 17
      .=TRUE by BINARITH:10;
  end;
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;
  let z be Element of Y;
A2: Ex('not' b,PA,G) = B_SUP('not' b,CompF(PA,G)) by BVFUNC_2:def 10;
A3: (a.z '&' 'not' b.z)=TRUE or (a.z '&' 'not' b.z)=FALSE by XBOOLEAN:def 3;
A4: (a 'xor' b).z =a.z 'xor' b.z by BVFUNC_1:def 5
    .=('not' a.z '&' b.z) 'or' (a.z '&' 'not' b.z);
A5: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
A6: FALSE '&' TRUE =FALSE by MARGREL1:13;
  assume
A7: (a 'xor' b).z=TRUE;
  per cases by A7,A4,A3,BINARITH:3;
  suppose
A8: ('not' a.z '&' b.z)=TRUE;
    then 'not' a.z=TRUE by MARGREL1:12;
    then ('not' a).z=TRUE by MARGREL1:def 19;
    then
A9: B_SUP('not' a,CompF(PA,G)).z = TRUE by A5,BVFUNC_1:def 17;
A10: ('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z ='not' (Ex(a,PA,G)
    'xor' Ex('not' b,PA,G)).z by MARGREL1:def 19;
    b.z=TRUE by A8,MARGREL1:12;
    then B_SUP(b,CompF(PA,G)).z = TRUE by A5,BVFUNC_1:def 17;
    then
A11: Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10;
A12: (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)).z =Ex('not' a,PA,G).z 'xor' Ex(b,
    PA,G).z by BVFUNC_1:def 5
      .=FALSE by A1,A6,A9,A11,MARGREL1:11;
    thus ('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)) 'or' 'not' (Ex(a,PA,G)
'xor' Ex('not' b,PA,G))).z =('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G))).z 'or'
    ('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z by BVFUNC_1:def 4
      .='not' FALSE 'or' 'not' ((Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z by A12
,A10,MARGREL1:def 19
      .=TRUE 'or' 'not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G)).z by MARGREL1:11
      .=TRUE by BINARITH:10;
  end;
  suppose
A13: (a.z '&' 'not' b.z)=TRUE;
    then a.z=TRUE by MARGREL1:12;
    then B_SUP(a,CompF(PA,G)).z = TRUE by A5,BVFUNC_1:def 17;
    then
A14: Ex(a,PA,G).z=TRUE by BVFUNC_2:def 10;
A15: ('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z ='not' ((Ex(a,PA,G)
    'xor' Ex('not' b,PA,G))).z by MARGREL1:def 19;
    'not' b.z=TRUE by A13,MARGREL1:12;
    then ('not' b).z=TRUE by MARGREL1:def 19;
    then
A16: B_SUP('not' b,CompF(PA,G)).z = TRUE by A5,BVFUNC_1:def 17;
A17: (Ex(a,PA,G) 'xor' Ex('not' b,PA,G)).z =Ex(a,PA,G).z 'xor' Ex('not' b,
    PA,G).z by BVFUNC_1:def 5
      .=FALSE by A2,A6,A16,A14,MARGREL1:11;
    thus ('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)) 'or' 'not' (Ex(a,PA,G)
'xor' Ex('not' b,PA,G))).z =('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G))).z 'or'
    ('not' (Ex(a,PA,G) 'xor' Ex('not' b,PA,G))).z by BVFUNC_1:def 4
      .='not' ((Ex('not' a,PA,G) 'xor' Ex(b,PA,G))).z 'or' 'not' FALSE by A17
,A15,MARGREL1:def 19
      .='not' ((Ex('not' a,PA,G) 'xor' Ex(b,PA,G))).z 'or' TRUE by MARGREL1:11
      .=TRUE by BINARITH:10;
  end;
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: 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
    (a 'or' b).x=TRUE);
    then B_INF(a 'or' b,CompF(PA,G)).z=FALSE by BVFUNC_1:def 16;
    hence contradiction by A1,BVFUNC_2:def 9;
  end;
  per cases;
  suppose
    ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE;
    then B_SUP(b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17;
    then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10;
    hence (All(a,PA,G) 'or' Ex(b,PA,G)) .z =All(a,PA,G).z 'or' TRUE by
BVFUNC_1:def 4
      .=TRUE by BINARITH:10;
  end;
  suppose
    (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.
x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=
    TRUE);
    then B_INF(a,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
    then All(a,PA,G).z=TRUE by BVFUNC_2:def 9;
    hence (All(a,PA,G) 'or' Ex(b,PA,G)) .z =TRUE 'or' Ex(b,PA,G).z by
BVFUNC_1:def 4
      .=TRUE by BINARITH:10;
  end;
  suppose
A3: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
    b.x=TRUE);
    then consider x1 being Element of Y such that
A4: x1 in EqClass(z,CompF(PA,G)) and
A5: a.x1<>TRUE;
A6: b.x1<>TRUE by A3,A4;
A7: a.x1=FALSE by A5,XBOOLEAN:def 3;
    (a 'or' b).x1 = a.x1 'or' b.x1 by BVFUNC_1:def 4
      .= FALSE 'or' FALSE by A6,A7,XBOOLEAN:def 3
      .= FALSE;
    hence thesis by A2,A4;
  end;
end;

Lm1: now
  let Y,a,b,G,PA;
  let z be Element of Y;
  assume
A1: 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 (
  a 'or' b).x=TRUE);
  then B_INF(a 'or' b,CompF(PA,G)).z=FALSE by BVFUNC_1:def 16;
  hence contradiction by A1,BVFUNC_2:def 9;
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: 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)) & a.x=TRUE;
    then B_SUP(a,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17;
    then Ex(a,PA,G).z=TRUE by BVFUNC_2:def 10;
    hence (Ex(a,PA,G) 'or' All(b,PA,G)) .z = TRUE 'or' All(b,PA,G).z by
BVFUNC_1:def 4
      .=TRUE by BINARITH:10;
  end;
  suppose
    (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x
=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=TRUE
    );
    then B_INF(b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
    then All(b,PA,G).z=TRUE by BVFUNC_2:def 9;
    hence (Ex(a,PA,G) 'or' All(b,PA,G)) .z =Ex(a,PA,G).z 'or' TRUE by
BVFUNC_1:def 4
      .=TRUE by BINARITH:10;
  end;
  suppose
A2: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds b.x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
    a.x=TRUE);
    then consider x1 being Element of Y such that
A3: x1 in EqClass(z,CompF(PA,G)) and
A4: b.x1<>TRUE;
A5: a.x1<>TRUE by A2,A3;
A6: b.x1=FALSE by A4,XBOOLEAN:def 3;
    (a 'or' b).x1 = a.x1 'or' b.x1 by BVFUNC_1:def 4
      .= FALSE 'or' FALSE by A5,A6,XBOOLEAN:def 3
      .= FALSE;
    hence thesis by A1,A3,Lm1;
  end;
end;

theorem
  All(a 'or' b,PA,G) '<' Ex(a,PA,G) 'or' Ex(b,PA,G)
proof
  let z be Element of Y;
A1: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
  assume All(a 'or' b,PA,G).z=TRUE;
  then (a 'or' b).z=TRUE by A1,Lm1;
  then
A2: a.z 'or' b.z=TRUE by BVFUNC_1:def 4;
A3: a.z=TRUE or a.z=FALSE by XBOOLEAN:def 3;
  per cases by A2,A3,BINARITH:3;
  suppose
    a.z=TRUE;
    then B_SUP(a,CompF(PA,G)).z = TRUE by A1,BVFUNC_1:def 17;
    then Ex(a,PA,G).z=TRUE by BVFUNC_2:def 10;
    hence (Ex(a,PA,G) 'or' Ex(b,PA,G)).z =TRUE 'or' Ex(b,PA,G).z by
BVFUNC_1:def 4
      .=TRUE by BINARITH:10;
  end;
  suppose
    b.z=TRUE;
    then B_SUP(b,CompF(PA,G)).z = TRUE by A1,BVFUNC_1:def 17;
    then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10;
    hence (Ex(a,PA,G) 'or' Ex(b,PA,G)).z =Ex(a,PA,G).z 'or' TRUE by
BVFUNC_1:def 4
      .=TRUE by BINARITH:10;
  end;
end;

theorem
  Ex(a,PA,G) '&' All(b,PA,G) '<' Ex(a '&' b,PA,G)
proof
  let z be Element of Y;
  assume (Ex(a,PA,G) '&' All(b,PA,G)) .z=TRUE;
  then
A1: Ex(a,PA,G).z '&' All(b,PA,G).z=TRUE by MARGREL1:def 20;
A2: now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
    holds b.x=TRUE);
    then B_INF(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(b,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  now
    assume
    not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x= TRUE);
    then B_SUP(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    then Ex(a,PA,G).z=FALSE by BVFUNC_2:def 10;
    hence contradiction by A1,MARGREL1:12;
  end;
  then consider x1 being Element of Y such that
A3: x1 in EqClass(z,CompF(PA,G)) and
A4: a.x1=TRUE;
  (a '&' b).x1 =a.x1 '&' b.x1 by MARGREL1:def 20
    .=TRUE '&' TRUE by A3,A4,A2
    .=TRUE;
  then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A3,BVFUNC_1:def 17;
  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 (All(a,PA,G) '&' Ex(b,PA,G)) .z=TRUE;
  then
A1: All(a,PA,G).z '&' Ex(b,PA,G).z=TRUE by MARGREL1:def 20;
A2: now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
    holds a.x=TRUE);
    then B_INF(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(a,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  now
    assume
    not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x= TRUE);
    then B_SUP(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    then Ex(b,PA,G).z=FALSE by BVFUNC_2:def 10;
    hence contradiction by A1,MARGREL1:12;
  end;
  then consider x1 being Element of Y such that
A3: x1 in EqClass(z,CompF(PA,G)) and
A4: b.x1=TRUE;
  (a '&' b).x1 =a.x1 '&' b.x1 by MARGREL1:def 20
    .=TRUE '&' TRUE by A3,A4,A2
    .=TRUE;
  then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A3,BVFUNC_1:def 17;
  hence thesis by BVFUNC_2:def 10;
end;

Lm2: now
  let Y,a,b,G,PA;
  let z be Element of Y;
  assume
A1: 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 (
  a 'imp' b).x=TRUE);
  then B_INF(a 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
  hence contradiction by A1,BVFUNC_2:def 9;
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: All(a 'imp' b,PA,G).z=TRUE;
A3: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
  per cases;
  suppose
    ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE;
    then B_SUP(b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17;
    then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10;
    hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by
BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
  suppose
    (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds a.x
=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE
    );
    then
A4: b.z<>TRUE & a.z=TRUE by A3;
    (a 'imp' b).z =('not' a.z) 'or' b.z by BVFUNC_1:def 8
      .=('not' TRUE) 'or' FALSE by A4,XBOOLEAN:def 3
      .=FALSE 'or' FALSE by MARGREL1:11
      .=FALSE;
    hence thesis by A2,A3,Lm2;
  end;
  suppose
A5: not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
holds a.x=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
    b.x=TRUE);
    thus (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' Ex(b,PA,
    G).z by BVFUNC_1:def 8
      .=('not' FALSE) 'or' Ex(b,PA,G).z by A1,A5,BVFUNC_1:def 16
      .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11
      .=TRUE by BINARITH:10;
  end;
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: 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)) & b.x=TRUE;
    then B_SUP(b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17;
    then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10;
    hence (Ex(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' Ex(a,PA,G).z) 'or' TRUE by
BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
  suppose
A3: (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=TRUE
) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE);
    then consider x1 being Element of Y such that
A4: x1 in EqClass(z,CompF(PA,G)) and
A5: a.x1=TRUE;
A6: b.x1<>TRUE by A3,A4;
    (a 'imp' b).x1 =('not' a.x1) 'or' b.x1 by BVFUNC_1:def 8
      .=('not' TRUE) 'or' FALSE by A5,A6,XBOOLEAN:def 3
      .=FALSE 'or' FALSE by MARGREL1:11
      .=FALSE;
    hence thesis by A2,A4,Lm2;
  end;
  suppose
A7: not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x
=TRUE) & not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x=TRUE
    );
    thus (Ex(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' Ex(a,PA,G).z) 'or' Ex(b,PA,G)
    .z by BVFUNC_1:def 8
      .=('not' FALSE) 'or' Ex(b,PA,G).z by A1,A7,BVFUNC_1:def 17
      .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11
      .=TRUE by BINARITH:10;
  end;
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 (Ex(a,PA,G) 'imp' All(b,PA,G)).z=TRUE;
  then
A1: ('not' Ex(a,PA,G).z) 'or' All(b,PA,G).z=TRUE by BVFUNC_1:def 8;
  per cases;
  suppose
A2: for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x= TRUE;
    for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp'
    b).x=TRUE
    proof
      let x be Element of Y;
      assume
A3:   x in EqClass(z,CompF(PA,G));
      thus (a 'imp' b).x=('not' a.x) 'or' b.x by BVFUNC_1:def 8
        .=('not' a.x) 'or' TRUE by A2,A3
        .=TRUE by BINARITH:10;
    end;
    then B_INF(a 'imp' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
    hence thesis by BVFUNC_2:def 9;
  end;
  suppose
A4: (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x=TRUE
) & not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x=TRUE
    );
    then B_SUP(a,CompF(PA,G)).z = TRUE by BVFUNC_1:def 17;
    then Ex(a,PA,G).z=TRUE by BVFUNC_2:def 10;
    then
A5: 'not' Ex(a,PA,G).z=FALSE by MARGREL1:11;
    B_INF(b,CompF(PA,G)).z = FALSE by A4,BVFUNC_1:def 16;
    then All(b,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence thesis by A1,A5;
  end;
  suppose
A6: not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x
=TRUE) & not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds b.x
    =TRUE);
    now
      let x be Element of Y;
      assume x in EqClass(z,CompF(PA,G));
      then
A7:   a.x<>TRUE by A6;
      thus (a 'imp' b).x =('not' a.x) 'or' b.x by BVFUNC_1:def 8
        .=('not' FALSE) 'or' b.x by A7,XBOOLEAN:def 3
        .=TRUE 'or' b.x by MARGREL1:11
        .=TRUE by BINARITH:10;
    end;
    then B_INF(a 'imp' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
    hence thesis by BVFUNC_2:def 9;
  end;
end;

theorem
  (a 'imp' b) '<' (a 'imp' Ex(b,PA,G))
proof
  let z be Element of Y;
A1: ('not' a.z)=TRUE or ('not' a.z)=FALSE by XBOOLEAN:def 3;
A2: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
  assume (a 'imp' b).z=TRUE;
  then
A3: ('not' a.z) 'or' b.z=TRUE by BVFUNC_1:def 8;
  per cases by A3,A1,BINARITH:3;
  suppose
    'not' a.z=TRUE;
    hence (a 'imp' Ex(b,PA,G)).z =TRUE 'or' Ex(b,PA,G).z by BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
  suppose
    b.z=TRUE;
    then B_SUP(b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17;
    then Ex(b,PA,G).z =TRUE by BVFUNC_2:def 10;
    hence (a 'imp' Ex(b,PA,G)).z =('not' a.z) 'or' TRUE by BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
end;

theorem
  (a 'imp' b) '<' (All(a,PA,G) 'imp' b)
proof
  let z be Element of Y;
A1: ('not' a.z)=TRUE or ('not' a.z)=FALSE by XBOOLEAN:def 3;
A2: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
  assume (a 'imp' b).z=TRUE;
  then
A3: ('not' a.z) 'or' b.z=TRUE by BVFUNC_1:def 8;
  per cases by A3,A1,BINARITH:3;
  suppose
    'not' a.z=TRUE;
    then a.z=FALSE by MARGREL1:11;
    then B_INF(a,CompF(PA,G)).z = FALSE by A2,BVFUNC_1:def 16;
    then All(a,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence (All(a,PA,G) 'imp' b).z =('not' FALSE) 'or' b.z by BVFUNC_1:def 8
      .=TRUE 'or' b.z by MARGREL1:11
      .=TRUE by BINARITH:10;
  end;
  suppose
    b.z=TRUE;
    hence (All(a,PA,G) 'imp' b).z =('not' All(a,PA,G).z) 'or' TRUE by
BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
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: 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)) & (a
    'imp' b).x=TRUE);
    then B_SUP(a 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    hence contradiction by A1,BVFUNC_2:def 10;
  end;
  then consider x1 being Element of Y such that
A2: x1 in EqClass(z,CompF(PA,G)) and
A3: (a 'imp' b).x1=TRUE;
A4: ('not' a.x1) 'or' b.x1=TRUE by A3,BVFUNC_1:def 8;
A5: b.x1=TRUE or b.x1=FALSE by XBOOLEAN:def 3;
  per cases by A4,A5,BINARITH:3;
  suppose
    ('not' a.x1)=TRUE;
    then a.x1=FALSE by MARGREL1:11;
    then B_INF(a,CompF(PA,G)).z = FALSE by A2,BVFUNC_1:def 16;
    then All(a,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' FALSE) 'or' Ex(b,PA,G).z by
BVFUNC_1:def 8
      .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11
      .=TRUE by BINARITH:10;
  end;
  suppose
    b.x1=TRUE;
    then B_SUP(b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17;
    then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10;
    hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by
BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
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: 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
    a.x=TRUE);
    then B_INF(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    hence contradiction by A1,BVFUNC_2:def 9;
  end;
  per cases;
  suppose
A3: Ex(b,PA,G).z=TRUE;
    now
      assume
      not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b. x=TRUE);
      then B_SUP(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
      hence contradiction by A3,BVFUNC_2:def 10;
    end;
    then consider x1 being Element of Y such that
A4: x1 in EqClass(z,CompF(PA,G)) and
A5: b.x1=TRUE;
    (a '&' b).x1 =a.x1 '&' b.x1 by MARGREL1:def 20
      .=TRUE '&' TRUE by A2,A4,A5
      .=TRUE;
    then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A4,BVFUNC_1:def 17;
    then Ex(a '&' b,PA,G).z=TRUE by BVFUNC_2:def 10;
    hence
    (Ex(b,PA,G) 'imp' Ex(a '&' b,PA,G)).z =('not' Ex(b,PA,G).z) 'or' TRUE
    by BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
  suppose
    Ex(b,PA,G).z<>TRUE;
    then Ex(b,PA,G).z=FALSE by XBOOLEAN:def 3;
    hence
    (Ex(b,PA,G) 'imp' Ex(a '&' b,PA,G)).z =('not' FALSE) 'or' Ex(a '&' b,
    PA,G).z by BVFUNC_1:def 8
      .=TRUE 'or' Ex(a '&' b,PA,G).z by MARGREL1:11
      .=TRUE by BINARITH:10;
  end;
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;
A2: z in EqClass(z,CompF(PA,G)) & EqClass(z,CompF(PA,G)) in CompF(PA,G) by
EQREL_1:def 6;
  assume
A3: 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)) & (u
    'imp' a).x=TRUE);
    then B_SUP(u 'imp' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    hence contradiction by A3,BVFUNC_2:def 10;
  end;
  then consider x1 being Element of Y such that
A4: x1 in EqClass(z,CompF(PA,G)) and
A5: (u 'imp' a).x1=TRUE;
A6: ('not' u.x1) 'or' a.x1=TRUE by A5,BVFUNC_1:def 8;
A7: ('not' u.x1)=TRUE or ('not' u.x1)=FALSE by XBOOLEAN:def 3;
  per cases by A6,A7,BINARITH:3;
  suppose
A8: ('not' u.x1)=TRUE;
    u.x1 = u.z by A1,A4,A2;
    then u.z=FALSE by A8,MARGREL1:11;
    hence (u 'imp' Ex(a,PA,G)).z =('not' FALSE) 'or' Ex(a,PA,G).z by
BVFUNC_1:def 8
      .=TRUE 'or' Ex(a,PA,G).z by MARGREL1:11
      .=TRUE by BINARITH:10;
  end;
  suppose
    a.x1=TRUE;
    then B_SUP(a,CompF(PA,G)).z = TRUE by A4,BVFUNC_1:def 17;
    then Ex(a,PA,G).z=TRUE by BVFUNC_2:def 10;
    hence (u 'imp' Ex(a,PA,G)).z =('not' u.z) 'or' TRUE by BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
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;
A2: z in EqClass(z,CompF(PA,G)) & EqClass(z,CompF(PA,G)) in CompF(PA,G) by
EQREL_1:def 6;
  assume
A3: 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)) & (a
    'imp' u).x=TRUE);
    then B_SUP(a 'imp' u,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    hence contradiction by A3,BVFUNC_2:def 10;
  end;
  then consider x1 being Element of Y such that
A4: x1 in EqClass(z,CompF(PA,G)) and
A5: (a 'imp' u).x1=TRUE;
A6: ('not' a.x1) 'or' u.x1=TRUE by A5,BVFUNC_1:def 8;
A7: ('not' a.x1)=TRUE or ('not' a.x1)=FALSE by XBOOLEAN:def 3;
  per cases by A6,A7,BINARITH:3;
  suppose
    ('not' a.x1)=TRUE;
    then a.x1=FALSE by MARGREL1:11;
    then B_INF(a,CompF(PA,G)).z = FALSE by A4,BVFUNC_1:def 16;
    then All(a,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence (All(a,PA,G) 'imp' u).z =('not' FALSE) 'or' u.z by BVFUNC_1:def 8
      .=TRUE 'or' u.z by MARGREL1:11
      .=TRUE by BINARITH:10;
  end;
  suppose
A8: u.x1=TRUE;
    u.x1 = u.z by A1,A4,A2;
    hence (All(a,PA,G) 'imp' u).z =('not' All(a,PA,G).z) 'or' TRUE by A8,
BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
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;
A3: ('not' All(a,PA,G).z)=TRUE or ('not' All(a,PA,G).z)=FALSE by XBOOLEAN:def 3
;
    assume (All(a,PA,G) 'imp' Ex(b,PA,G)).z=TRUE;
    then
A4: ('not' All(a,PA,G).z) 'or' Ex(b,PA,G).z=TRUE by BVFUNC_1:def 8;
    per cases by A4,A3,BINARITH:3;
    suppose
      ('not' All(a,PA,G).z)=TRUE;
      then All(a,PA,G).z=FALSE by MARGREL1:11;
      then consider x1 being Element of Y such that
A5:   x1 in EqClass(z,CompF(PA,G)) and
A6:   a.x1<>TRUE by A1,BVFUNC_1:def 16;
      (a 'imp' b).x1 =('not' a.x1) 'or' b.x1 by BVFUNC_1:def 8
        .=('not' FALSE) 'or' b.x1 by A6,XBOOLEAN:def 3
        .=TRUE 'or' b.x1 by MARGREL1:11
        .=TRUE by BINARITH:10;
      then B_SUP(a 'imp' b,CompF(PA,G)).z = TRUE by A5,BVFUNC_1:def 17;
      hence thesis by BVFUNC_2:def 10;
    end;
    suppose
A7:   Ex(b,PA,G).z=TRUE;
      now
        assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) &
        b.x=TRUE);
        then B_SUP(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
        hence contradiction by A7,BVFUNC_2:def 10;
      end;
      then consider x1 being Element of Y such that
A8:   x1 in EqClass(z,CompF(PA,G)) and
A9:   b.x1=TRUE;
      (a 'imp' b).x1 =('not' a.x1) 'or' TRUE by A9,BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
      then B_SUP(a 'imp' b,CompF(PA,G)).z = TRUE by A8,BVFUNC_1:def 17;
      hence thesis by BVFUNC_2:def 10;
    end;
  end;
  Ex(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G)
  proof
    let z be Element of Y;
    assume
A10: 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)) & (
      a 'imp' b).x=TRUE);
      then B_SUP(a 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
      hence contradiction by A10,BVFUNC_2:def 10;
    end;
    then consider x1 being Element of Y such that
A11: x1 in EqClass(z,CompF(PA,G)) and
A12: (a 'imp' b).x1=TRUE;
A13: ('not' a.x1) 'or' b.x1=TRUE by A12,BVFUNC_1:def 8;
A14: ('not' a.x1)=TRUE or ('not' a.x1)=FALSE by XBOOLEAN:def 3;
    per cases by A13,A14,BINARITH:3;
    suppose
      ('not' a.x1)=TRUE;
      then a.x1=FALSE by MARGREL1:11;
      then B_INF(a,CompF(PA,G)).z = FALSE by A11,BVFUNC_1:def 16;
      hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' FALSE) 'or' Ex(b,PA,G).z
      by A1,BVFUNC_1:def 8
        .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11
        .=TRUE by BINARITH:10;
    end;
    suppose
      b.x1=TRUE;
      then B_SUP(b,CompF(PA,G)).z = TRUE by A11,BVFUNC_1:def 17;
      then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10;
      hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE
      by BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
    end;
  end;
  hence thesis by A2,BVFUNC_1:15;
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;
A1: ('not' All(a,PA,G).z)=TRUE or ('not' All(a,PA,G).z)=FALSE by XBOOLEAN:def 3
;
A2: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
  assume (All(a,PA,G) 'imp' All(b,PA,G)).z=TRUE;
  then
A3: ('not' All(a,PA,G).z) 'or' All(b,PA,G).z=TRUE by BVFUNC_1:def 8;
  per cases by A3,A1,BINARITH:3;
  suppose
    'not' All(a,PA,G).z=TRUE;
    hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =TRUE 'or' Ex(b,PA,G).z by
BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
  suppose
A4: All(b,PA,G).z=TRUE;
    now
      assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
      holds b.x=TRUE);
      then B_INF(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
      hence contradiction by A4,BVFUNC_2:def 9;
    end;
    then b.z=TRUE by A2;
    then B_SUP(b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17;
    then Ex(b,PA,G).z=TRUE by BVFUNC_2:def 10;
    hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by
BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
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;
A2: ('not' Ex(a,PA,G).z)=TRUE or ('not' Ex(a,PA,G).z)=FALSE by XBOOLEAN:def 3;
  assume (Ex(a,PA,G) 'imp' Ex(b,PA,G)).z=TRUE;
  then
A3: ('not' Ex(a,PA,G).z) 'or' Ex(b,PA,G).z=TRUE by BVFUNC_1:def 8;
A4: z in EqClass(z,CompF(PA,G)) by EQREL_1:def 6;
  per cases by A3,A2,BINARITH:3;
  suppose
    ('not' Ex(a,PA,G).z)=TRUE;
    then Ex(a,PA,G).z=FALSE by MARGREL1:11;
    then a.z<>TRUE by A1,A4,BVFUNC_1:def 17;
    then B_INF(a,CompF(PA,G)).z = FALSE by A4,BVFUNC_1:def 16;
    then All(a,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' FALSE) 'or' Ex(b,PA,G).z by
BVFUNC_1:def 8
      .=TRUE 'or' Ex(b,PA,G).z by MARGREL1:11
      .=TRUE by BINARITH:10;
  end;
  suppose
    Ex(b,PA,G).z=TRUE;
    hence (All(a,PA,G) 'imp' Ex(b,PA,G)).z =('not' All(a,PA,G).z) 'or' TRUE by
BVFUNC_1:def 8
      .=TRUE by BINARITH:10;
  end;
end;

theorem Th26:
  All(a 'imp' b,PA,G) = All('not' a 'or' b,PA,G)
proof
A1: All('not' a 'or' b,PA,G) '<' All(a 'imp' b,PA,G)
  proof
    let z be Element of Y;
    assume
A2: All('not' a 'or' b,PA,G).z=TRUE;
A3: now
      assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
      holds ('not' a 'or' b).x=TRUE);
      then B_INF('not' a 'or' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
      hence contradiction by A2,BVFUNC_2:def 9;
    end;
    for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a
    'imp' b).x=TRUE
    proof
      let x be Element of Y;
A4:   ('not' a).x=TRUE or ('not' a).x=FALSE by XBOOLEAN:def 3;
      assume x in EqClass(z,CompF(PA,G));
      then ('not' a 'or' b).x=TRUE by A3;
      then
A5:   ('not' a).x 'or' b.x=TRUE by BVFUNC_1:def 4;
      per cases by A5,A4,BINARITH:3;
      suppose
        ('not' a).x=TRUE;
        then 'not' a.x=TRUE by MARGREL1:def 19;
        hence (a 'imp' b).x = TRUE 'or' b.x by BVFUNC_1:def 8
          .=TRUE by BINARITH:10;
      end;
      suppose
        b.x=TRUE;
        hence (a 'imp' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8
          .=TRUE by BINARITH:10;
      end;
    end;
    then B_INF(a 'imp' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
    hence thesis by BVFUNC_2:def 9;
  end;
  All(a 'imp' b,PA,G) '<' All('not' a 'or' b,PA,G)
  proof
    let z be Element of Y;
    assume
A6: All(a 'imp' b,PA,G).z=TRUE;
A7: now
      assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
      holds (a 'imp' b).x=TRUE);
      then B_INF(a 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
      hence contradiction by A6,BVFUNC_2:def 9;
    end;
    now
      let x be Element of Y;
A8:   ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3;
      assume x in EqClass(z,CompF(PA,G));
      then (a 'imp' b).x=TRUE by A7;
      then
A9:   ('not' a.x) 'or' b.x=TRUE by BVFUNC_1:def 8;
      per cases by A9,A8,BINARITH:3;
      suppose
        ('not' a.x)=TRUE;
        then ('not' a).x=TRUE by MARGREL1:def 19;
        hence ('not' a 'or' b).x =TRUE 'or' b.x by BVFUNC_1:def 4
          .=TRUE by BINARITH:10;
      end;
      suppose
        b.x=TRUE;
        hence ('not' a 'or' b).x=('not' a).x 'or' TRUE by BVFUNC_1:def 4
          .=TRUE by BINARITH:10;
      end;
    end;
    then B_INF('not' a 'or' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
    hence thesis by BVFUNC_2:def 9;
  end;
  hence thesis by A1,BVFUNC_1:15;
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) & 'not'
  ( 'not' a 'or' b)=('not' 'not' a) '&' ('not' b) by BVFUNC_1:13,BVFUNC_2:18;
  hence thesis by 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;
A1: ('not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G))).z ='not' ((
  All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G))).z by MARGREL1:def 19
    .='not' (All(a 'imp' b,PA,G).z '&' (All(a 'imp' 'not' b,PA,G)).z) by
MARGREL1:def 20;
  assume
A2: Ex(a,PA,G).z=TRUE;
  now
    assume
    not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x= TRUE);
    then B_SUP(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    hence contradiction by A2,BVFUNC_2:def 10;
  end;
  then consider x1 being Element of Y such that
A3: x1 in EqClass(z,CompF(PA,G)) and
A4: a.x1=TRUE;
A5: (a 'imp' b).x1 ='not' TRUE 'or' b.x1 by A4,BVFUNC_1:def 8
    .=FALSE 'or' b.x1 by MARGREL1:11
    .=b.x1 by BINARITH:3;
A6: (a 'imp' 'not' b).x1 ='not' TRUE 'or' ('not' b).x1 by A4,BVFUNC_1:def 8
    .=FALSE 'or' ('not' b).x1 by MARGREL1:11
    .=('not' b).x1 by BINARITH:3;
  per cases by XBOOLEAN:def 3;
  suppose
    b.x1=TRUE;
    then (a 'imp' 'not' b).x1 ='not' TRUE by A6,MARGREL1:def 19
      .=FALSE by MARGREL1:11;
    then (B_INF(a 'imp' 'not' b,CompF(PA,G))).z = FALSE by A3,BVFUNC_1:def 16;
    hence ('not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G))).z ='not'
    (All(a 'imp' b,PA,G).z '&' FALSE) by A1,BVFUNC_2:def 9
      .='not' (FALSE) by MARGREL1:12
      .=TRUE by MARGREL1:11;
  end;
  suppose
    b.x1=FALSE;
    then B_INF(a 'imp' b,CompF(PA,G)).z = FALSE by A3,A5,BVFUNC_1:def 16;
    hence ('not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G))).z ='not'
    (FALSE '&' (All(a 'imp' 'not' b,PA,G)).z) by A1,BVFUNC_2:def 9
      .='not' (FALSE) by MARGREL1:12
      .=TRUE by MARGREL1:11;
  end;
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;
A1: ('not' Ex(a '&' 'not' b,PA,G)).z='not' (Ex(a '&' 'not' b,PA,G)).z by
MARGREL1:def 19;
A2: ('not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G))).z =
'not' (('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G))).z by
MARGREL1:def 19
    .='not' (('not' Ex(a '&' b,PA,G)).z '&' ('not' Ex(a '&' 'not' b,PA,G)).z
  ) by MARGREL1:def 20
    .='not' ('not' Ex(a '&' b,PA,G).z '&' 'not' (Ex(a '&' 'not' b,PA,G)).z)
  by A1,MARGREL1:def 19;
  assume
A3: Ex(a,PA,G).z=TRUE;
  now
    assume
    not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x= TRUE);
    then B_SUP(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    hence contradiction by A3,BVFUNC_2:def 10;
  end;
  then consider x1 being Element of Y such that
A4: x1 in EqClass(z,CompF(PA,G)) and
A5: a.x1=TRUE;
A6: (a '&' b).x1 =TRUE '&' b.x1 by A5,MARGREL1:def 20
    .=b.x1 by MARGREL1:14;
A7: (a '&' 'not' b).x1 =TRUE '&' ('not' b).x1 by A5,MARGREL1:def 20
    .=('not' b).x1 by MARGREL1:14;
  per cases by XBOOLEAN:def 3;
  suppose
    b.x1=TRUE;
    then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A4,A6,BVFUNC_1:def 17;
    hence
    ('not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G))).z =
    'not' ('not' TRUE '&' 'not' (Ex(a '&' 'not' b,PA,G)).z) by A2,
BVFUNC_2:def 10
      .='not' (FALSE '&' 'not' (Ex(a '&' 'not' b,PA,G)).z) by MARGREL1:11
      .='not' (FALSE) by MARGREL1:12
      .=TRUE by MARGREL1:11;
  end;
  suppose
    b.x1=FALSE;
    then (a '&' 'not' b).x1='not' FALSE by A7,MARGREL1:def 19;
    then (a '&' 'not' b).x1=TRUE by MARGREL1:11;
    then (B_SUP(a '&' 'not' b,CompF(PA,G))).z = TRUE by A4,BVFUNC_1:def 17;
    hence
    ('not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G))).z =
    'not' ('not' Ex(a '&' b,PA,G).z '&' 'not' TRUE) by A2,BVFUNC_2:def 10
      .='not' ('not' Ex(a '&' b,PA,G).z '&' FALSE) by MARGREL1:11
      .='not' (FALSE) by MARGREL1:12
      .=TRUE by MARGREL1:11;
  end;
end;

theorem
  Ex(a,PA,G) '&' All(a 'imp' b,PA,G) '<' Ex(a '&' b,PA,G)
proof
  let z be Element of Y;
A1: 'not' FALSE=TRUE by MARGREL1:11;
  assume (Ex(a,PA,G) '&' All(a 'imp' b,PA,G)).z=TRUE;
  then
A2: Ex(a,PA,G).z '&' All(a 'imp' b,PA,G).z=TRUE by MARGREL1:def 20;
  now
    assume
    not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x= TRUE);
    then B_SUP(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    then Ex(a,PA,G).z=FALSE by BVFUNC_2:def 10;
    hence contradiction by A2,MARGREL1:12;
  end;
  then consider x1 being Element of Y such that
A3: x1 in EqClass(z,CompF(PA,G)) and
A4: a.x1=TRUE;
  now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
    holds (a 'imp' b).x=TRUE);
    then B_INF(a 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(a 'imp' b,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A2,MARGREL1:12;
  end;
  then (a 'imp' b).x1=TRUE by A3;
  then
A5: ('not' a.x1) 'or' b.x1 =TRUE by BVFUNC_1:def 8;
  (a '&' b).x1 =a.x1 '&' b.x1 by MARGREL1:def 20
    .=TRUE '&' TRUE by A4,A5,A1,BINARITH:3
    .=TRUE;
  then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A3,BVFUNC_1:def 17;
  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
  let z be Element of Y;
  assume (Ex(a,PA,G) '&' 'not' Ex(a '&' b,PA,G)).z=TRUE;
  then
A1: Ex(a,PA,G).z '&' ('not' Ex(a '&' b,PA,G)).z=TRUE by MARGREL1:def 20;
  now
    assume
    not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & a.x= TRUE);
    then B_SUP(a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    then Ex(a,PA,G).z=FALSE by BVFUNC_2:def 10;
    hence contradiction by A1,MARGREL1:12;
  end;
  then consider x1 being Element of Y such that
A2: x1 in EqClass(z,CompF(PA,G)) and
A3: a.x1=TRUE;
  ('not' Ex(a '&' b,PA,G)).z=TRUE by A1,MARGREL1:12;
  then 'not' Ex(a '&' b,PA,G).z=TRUE by MARGREL1:def 19;
  then
  Ex(a '&' b,PA,G) = B_SUP(a '&' b,CompF(PA,G)) & Ex(a '&' b,PA,G).z=FALSE
  by BVFUNC_2:def 10,MARGREL1:11;
  then (a '&' b).x1<>TRUE by A2,BVFUNC_1:def 17;
  then (a '&' b).x1=FALSE by XBOOLEAN:def 3;
  then
A4: a.x1 '&' b.x1=FALSE by MARGREL1:def 20;
  per cases by A4,MARGREL1:12;
  suppose
    a.x1=FALSE;
    hence thesis by A3;
  end;
  suppose
    b.x1=FALSE;
    then (a 'imp' b).x1 =('not' TRUE) 'or' FALSE by A3,BVFUNC_1:def 8
      .=FALSE 'or' FALSE by MARGREL1:11
      .=FALSE;
    then B_INF(a 'imp' b,CompF(PA,G)).z = FALSE by A2,BVFUNC_1:def 16;
    then All(a 'imp' b,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence ('not' All(a 'imp' b,PA,G)).z ='not' FALSE by MARGREL1:def 19
      .=TRUE by MARGREL1:11;
  end;
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 (All(a 'imp' c,PA,G) '&' All(c 'imp' b,PA,G)).z=TRUE;
  then
A1: All(a 'imp' c,PA,G).z '&' All(c 'imp' b,PA,G).z=TRUE by MARGREL1:def 20;
A2: now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
    (c 'imp' b).x=TRUE);
    then B_INF(c 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(c 'imp' b,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
A3: now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
    (a 'imp' c).x=TRUE);
    then B_INF(a 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(a 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp'
  b).x=TRUE
  proof
    let x be Element of Y;
A4: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3;
A5: ('not' c.x)=TRUE or ('not' c.x)=FALSE by XBOOLEAN:def 3;
    assume
A6: x in EqClass(z,CompF(PA,G));
    then (a 'imp' c).x=TRUE by A3;
    then
A7: ('not' a.x) 'or' c.x=TRUE by BVFUNC_1:def 8;
    (c 'imp' b).x=TRUE by A2,A6;
    then
A8: ('not' c.x) 'or' b.x=TRUE by BVFUNC_1:def 8;
    per cases by A7,A4,A8,A5,BINARITH:3;
    suppose
      ('not' a.x)=TRUE & ('not' c.x)=TRUE;
      hence (a 'imp' b).x =TRUE 'or' b.x by BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
    end;
    suppose
      ('not' a.x)=TRUE & b.x=TRUE;
      hence (a 'imp' b).x =TRUE 'or' b.x by BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
    end;
    suppose
      c.x=TRUE & ('not' c.x)=TRUE;
      hence thesis by MARGREL1:11;
    end;
    suppose
      c.x=TRUE & b.x=TRUE;
      hence (a 'imp' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
    end;
  end;
  then B_INF(a 'imp' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
  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 (All(c 'imp' b,PA,G) '&' Ex(a '&' c,PA,G)).z=TRUE;
  then
A1: All(c 'imp' b,PA,G).z '&' Ex(a '&' c,PA,G).z=TRUE by MARGREL1:def 20;
  now
    assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & (a
    '&' c).x=TRUE);
    then B_SUP(a '&' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    then Ex(a '&' c,PA,G).z=FALSE by BVFUNC_2:def 10;
    hence contradiction by A1,MARGREL1:12;
  end;
  then consider x1 being Element of Y such that
A2: x1 in EqClass(z,CompF(PA,G)) and
A3: (a '&' c).x1=TRUE;
A4: a.x1 '&' c.x1=TRUE by A3,MARGREL1:def 20;
  now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
    (c 'imp' b).x=TRUE);
    then B_INF(c 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(c 'imp' b,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  then (c 'imp' b).x1=TRUE by A2;
  then
A5: ('not' c.x1) 'or' b.x1=TRUE by BVFUNC_1:def 8;
A6: ('not' c.x1)=TRUE or ('not' c.x1)=FALSE by XBOOLEAN:def 3;
  per cases by A5,A6,A4,BINARITH:3,MARGREL1:12;
  suppose
    a.x1=TRUE & c.x1=TRUE & ('not' c.x1)=TRUE;
    hence thesis by MARGREL1:11;
  end;
  suppose
    a.x1=TRUE & c.x1=TRUE & b.x1=TRUE;
    then (a '&' b).x1 =TRUE '&' TRUE by MARGREL1:def 20
      .=TRUE;
    then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17;
    hence thesis by BVFUNC_2:def 10;
  end;
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 (All(b 'imp' 'not' c,PA,G) '&' All(a 'imp' c,PA,G)).z=TRUE;
  then
A1: All(b 'imp' 'not' c,PA,G).z '&' All(a 'imp' c,PA,G).z=TRUE by
MARGREL1:def 20;
A2: now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
    (a 'imp' c).x=TRUE);
    then B_INF(a 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(a 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
A3: now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
    (b 'imp' 'not' c).x=TRUE);
    then B_INF(b 'imp' 'not' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(b 'imp' 'not' c,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp'
  'not' b).x=TRUE
  proof
    let x be Element of Y;
A4: ('not' b.x)=TRUE or ('not' b.x)=FALSE by XBOOLEAN:def 3;
A5: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3;
    assume
A6: x in EqClass(z,CompF(PA,G));
    then (b 'imp' 'not' c).x=TRUE by A3;
    then
A7: ('not' b.x) 'or' ('not' c).x=TRUE by BVFUNC_1:def 8;
    (a 'imp' c).x=TRUE by A2,A6;
    then
A8: ('not' a.x) 'or' c.x=TRUE by BVFUNC_1:def 8;
    per cases by A7,A4,A8,A5,BINARITH:3;
    suppose
A9:   ('not' b.x)=TRUE & ('not' a.x)=TRUE;
      then ('not' b).x=TRUE by MARGREL1:def 19;
      hence (a 'imp' 'not' b).x =TRUE 'or' TRUE by A9,BVFUNC_1:def 8
        .=TRUE;
    end;
    suppose
      ('not' b.x)=TRUE & c.x=TRUE;
      then ('not' b).x=TRUE by MARGREL1:def 19;
      hence (a 'imp' 'not' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
    end;
    suppose
      ('not' c).x=TRUE & ('not' a.x)=TRUE;
      hence (a 'imp' 'not' b).x =TRUE 'or' ('not' b).x by BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
    end;
    suppose
A10:  ('not' c).x=TRUE & c.x=TRUE;
      then 'not' c.x=TRUE by MARGREL1:def 19;
      hence thesis by A10,MARGREL1:11;
    end;
  end;
  then B_INF(a 'imp' 'not' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
  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 (All(b 'imp' c,PA,G) '&' All(a 'imp' 'not' c,PA,G)).z=TRUE;
  then
A1: All(b 'imp' c,PA,G).z '&' All(a 'imp' 'not' c,PA,G).z=TRUE by
MARGREL1:def 20;
A2: now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
    (a 'imp' 'not' c).x=TRUE);
    then B_INF(a 'imp' 'not' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(a 'imp' 'not' c,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
A3: now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
    (b 'imp' c).x=TRUE);
    then B_INF(b 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(b 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp'
  'not' b).x=TRUE
  proof
    let x be Element of Y;
A4: ('not' b.x)=TRUE or ('not' b.x)=FALSE by XBOOLEAN:def 3;
A5: ('not' a.x)=TRUE or ('not' a.x)=FALSE by XBOOLEAN:def 3;
    assume
A6: x in EqClass(z,CompF(PA,G));
    then (b 'imp' c).x=TRUE by A3;
    then
A7: ('not' b.x) 'or' c.x=TRUE by BVFUNC_1:def 8;
    (a 'imp' 'not' c).x=TRUE by A2,A6;
    then
A8: ('not' a.x) 'or' ('not' c).x=TRUE by BVFUNC_1:def 8;
    per cases by A7,A4,A8,A5,BINARITH:3;
    suppose
A9:   ('not' b.x)=TRUE & ('not' a.x)=TRUE;
      then ('not' b).x=TRUE by MARGREL1:def 19;
      hence (a 'imp' 'not' b).x =TRUE 'or' TRUE by A9,BVFUNC_1:def 8
        .=TRUE;
    end;
    suppose
      ('not' b.x)=TRUE & ('not' c).x=TRUE;
      then ('not' b).x=TRUE by MARGREL1:def 19;
      hence (a 'imp' 'not' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
    end;
    suppose
      c.x=TRUE & ('not' a.x)=TRUE;
      hence (a 'imp' 'not' b).x =TRUE 'or' ('not' b).x by BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
    end;
    suppose
A10:  c.x=TRUE & ('not' c).x=TRUE;
      then 'not' c.x=TRUE by MARGREL1:def 19;
      hence thesis by A10,MARGREL1:11;
    end;
  end;
  then B_INF(a 'imp' 'not' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
  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 (All(b 'imp' 'not' c,PA,G) '&' Ex(a '&' c,PA,G)).z=TRUE;
  then
A1: All(b 'imp' 'not' c,PA,G).z '&' Ex(a '&' c,PA,G).z=TRUE by MARGREL1:def 20;
  now
    assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & (a
    '&' c).x=TRUE);
    then B_SUP(a '&' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    then Ex(a '&' c,PA,G).z=FALSE by BVFUNC_2:def 10;
    hence contradiction by A1,MARGREL1:12;
  end;
  then consider x1 being Element of Y such that
A2: x1 in EqClass(z,CompF(PA,G)) and
A3: (a '&' c).x1=TRUE;
A4: a.x1 '&' c.x1=TRUE by A3,MARGREL1:def 20;
  now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
    (b 'imp' 'not' c).x=TRUE);
    then B_INF(b 'imp' 'not' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(b 'imp' 'not' c,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  then (b 'imp' 'not' c).x1=TRUE by A2;
  then
A5: ('not' b.x1) 'or' ('not' c).x1=TRUE by BVFUNC_1:def 8;
A6: ('not' b.x1)=TRUE or ('not' b.x1)=FALSE by XBOOLEAN:def 3;
  per cases by A5,A6,A4,BINARITH:3,MARGREL1:12;
  suppose
A7: a.x1=TRUE & c.x1=TRUE & ('not' b.x1)=TRUE;
    (a '&' 'not' b).x1 =a.x1 '&' ('not' b).x1 by MARGREL1:def 20
      .=TRUE '&' TRUE by A7,MARGREL1:def 19
      .=TRUE;
    then B_SUP(a '&' 'not' b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17;
    hence thesis by BVFUNC_2:def 10;
  end;
  suppose
A8: a.x1=TRUE & c.x1=TRUE & ('not' c).x1=TRUE;
    then 'not' c.x1=TRUE by MARGREL1:def 19;
    hence thesis by A8,MARGREL1:11;
  end;
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 (All(b 'imp' c,PA,G) '&' Ex(a '&' 'not' c,PA,G)).z=TRUE;
  then
A1: All(b 'imp' c,PA,G).z '&' Ex(a '&' 'not' c,PA,G).z=TRUE by MARGREL1:def 20;
  now
    assume not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & (a
    '&' 'not' c).x=TRUE);
    then B_SUP(a '&' 'not' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    then Ex(a '&' 'not' c,PA,G).z=FALSE by BVFUNC_2:def 10;
    hence contradiction by A1,MARGREL1:12;
  end;
  then consider x1 being Element of Y such that
A2: x1 in EqClass(z,CompF(PA,G)) and
A3: (a '&' 'not' c).x1=TRUE;
A4: a.x1 '&' ('not' c).x1=TRUE by A3,MARGREL1:def 20;
  now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
    (b 'imp' c).x=TRUE);
    then B_INF(b 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(b 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  then (b 'imp' c).x1=TRUE by A2;
  then
A5: ('not' b.x1) 'or' c.x1=TRUE by BVFUNC_1:def 8;
A6: ('not' b.x1)=TRUE or ('not' b.x1)=FALSE by XBOOLEAN:def 3;
  per cases by A5,A6,A4,BINARITH:3,MARGREL1:12;
  suppose
A7: a.x1=TRUE & ('not' c).x1=TRUE & ('not' b.x1)=TRUE;
    (a '&' 'not' b).x1 = a.x1 '&' ('not' b).x1 by MARGREL1:def 20
      .=TRUE '&' TRUE by A7,MARGREL1:def 19
      .=TRUE;
    then B_SUP(a '&' 'not' b,CompF(PA,G)).z = TRUE by A2,BVFUNC_1:def 17;
    hence thesis by BVFUNC_2:def 10;
  end;
  suppose
A8: a.x1=TRUE & ('not' c).x1=TRUE & c.x1=TRUE;
    then 'not' c.x1=TRUE by MARGREL1:def 19;
    hence thesis by A8,MARGREL1:11;
  end;
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 (Ex(c,PA,G) '&' All(c 'imp' b,PA,G) '&' All(c 'imp' a,PA,G)).z=TRUE;
  then
A1: (Ex(c,PA,G) '&' All(c 'imp' b,PA,G)).z '&' All(c 'imp' a,PA,G).z = TRUE
  by MARGREL1:def 20;
  then
  Ex(c,PA,G).z '&' All(c 'imp' b,PA,G).z '&' All(c 'imp' a,PA,G).z=TRUE by
MARGREL1:def 20;
  then
A2: Ex(c,PA,G).z '&' All(c 'imp' b,PA,G).z=TRUE by MARGREL1:12;
  now
    assume
    not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & c.x= TRUE);
    then B_SUP(c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    then Ex(c,PA,G).z=FALSE by BVFUNC_2:def 10;
    hence contradiction by A2,MARGREL1:12;
  end;
  then consider x1 being Element of Y such that
A3: x1 in EqClass(z,CompF(PA,G)) and
A4: c.x1=TRUE;
A5: ('not' c.x1)=TRUE or ('not' c.x1)=FALSE by XBOOLEAN:def 3;
  now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
    holds (c 'imp' b).x=TRUE);
    then B_INF(c 'imp' b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(c 'imp' b,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A2,MARGREL1:12;
  end;
  then (c 'imp' b).x1=TRUE by A3;
  then
A6: ('not' c.x1) 'or' b.x1=TRUE by BVFUNC_1:def 8;
  now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
    holds (c 'imp' a).x=TRUE);
    then B_INF(c 'imp' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(c 'imp' a,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  then (c 'imp' a).x1=TRUE by A3;
  then
A7: ('not' c.x1) 'or' a.x1=TRUE by BVFUNC_1:def 8;
  per cases by A7,A5,A6,BINARITH:3;
  suppose
    ('not' c.x1)=TRUE;
    hence thesis by A4,MARGREL1:11;
  end;
  suppose
    ('not' c.x1)=TRUE & b.x1=TRUE;
    hence thesis by A4,MARGREL1:11;
  end;
  suppose
    a.x1=TRUE & ('not' c.x1)=TRUE;
    hence thesis by A4,MARGREL1:11;
  end;
  suppose
    a.x1=TRUE & b.x1=TRUE;
    then (a '&' b).x1 =TRUE '&' TRUE by MARGREL1:def 20
      .=TRUE;
    then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A3,BVFUNC_1:def 17;
    hence thesis by BVFUNC_2:def 10;
  end;
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 (All(b 'imp' c,PA,G) '&' All(c 'imp' 'not' a,PA,G)).z=TRUE;
  then
A1: All(b 'imp' c,PA,G).z '&' All(c 'imp' 'not' a,PA,G).z=TRUE by
MARGREL1:def 20;
A2: now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
    (b 'imp' c).x=TRUE);
    then B_INF(b 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(b 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
A3: now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds
    (c 'imp' 'not' a).x=TRUE);
    then B_INF(c 'imp' 'not' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(c 'imp' 'not' a,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  for x being Element of Y st x in EqClass(z,CompF(PA,G)) holds (a 'imp'
  'not' b).x=TRUE
  proof
    let x be Element of Y;
A4: ('not' c.x)=TRUE or ('not' c.x)=FALSE by XBOOLEAN:def 3;
A5: ('not' b.x)=TRUE or ('not' b.x)=FALSE by XBOOLEAN:def 3;
    assume
A6: x in EqClass(z,CompF(PA,G));
    then (c 'imp' 'not' a).x=TRUE by A3;
    then
A7: ('not' c.x) 'or' ('not' a).x=TRUE by BVFUNC_1:def 8;
    (b 'imp' c).x=TRUE by A2,A6;
    then
A8: ('not' b.x) 'or' c.x=TRUE by BVFUNC_1:def 8;
    per cases by A7,A4,A8,A5,BINARITH:3;
    suppose
      ('not' c.x)=TRUE & ('not' b.x)=TRUE;
      then ('not' b).x=TRUE by MARGREL1:def 19;
      hence (a 'imp' 'not' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
    end;
    suppose
      ('not' c.x)=TRUE & c.x=TRUE;
      hence thesis by MARGREL1:11;
    end;
    suppose
      ('not' a).x=TRUE & ('not' b.x)=TRUE;
      then ('not' b).x=TRUE by MARGREL1:def 19;
      hence (a 'imp' 'not' b).x =('not' a.x) 'or' TRUE by BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
    end;
    suppose
      ('not' a).x=TRUE & c.x=TRUE;
      then 'not' a.x=TRUE by MARGREL1:def 19;
      hence (a 'imp' 'not' b).x =TRUE 'or' ('not' b).x by BVFUNC_1:def 8
        .=TRUE by BINARITH:10;
    end;
  end;
  then B_INF(a 'imp' 'not' b,CompF(PA,G)).z = TRUE by BVFUNC_1:def 16;
  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 (Ex(b,PA,G) '&' All(b 'imp' c,PA,G) '&' All(c 'imp' a,PA,G)).z=TRUE;
  then
A1: (Ex(b,PA,G) '&' All(b 'imp' c,PA,G)).z '&' All(c 'imp' a,PA,G).z= TRUE
  by MARGREL1:def 20;
  then
  Ex(b,PA,G).z '&' All(b 'imp' c,PA,G).z '&' All(c 'imp' a,PA,G).z=TRUE by
MARGREL1:def 20;
  then
A2: (Ex(b,PA,G).z '&' All(b 'imp' c,PA,G).z)=TRUE by MARGREL1:12;
  now
    assume
    not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & b.x= TRUE);
    then B_SUP(b,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    then Ex(b,PA,G).z=FALSE by BVFUNC_2:def 10;
    hence contradiction by A2,MARGREL1:12;
  end;
  then consider x1 being Element of Y such that
A3: x1 in EqClass(z,CompF(PA,G)) and
A4: b.x1=TRUE;
A5: ('not' c.x1)=TRUE or ('not' c.x1)=FALSE by XBOOLEAN:def 3;
  now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
    holds (c 'imp' a).x=TRUE);
    then B_INF(c 'imp' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(c 'imp' a,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  then (c 'imp' a).x1=TRUE by A3;
  then
A6: ('not' c.x1) 'or' a.x1=TRUE by BVFUNC_1:def 8;
A7: ('not' b.x1)=TRUE or ('not' b.x1)=FALSE by XBOOLEAN:def 3;
  now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
    holds (b 'imp' c).x=TRUE);
    then B_INF(b 'imp' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(b 'imp' c,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A2,MARGREL1:12;
  end;
  then (b 'imp' c).x1=TRUE by A3;
  then
A8: ('not' b.x1) 'or' c.x1=TRUE by BVFUNC_1:def 8;
  per cases by A6,A5,A8,A7,BINARITH:3;
  suppose
    ('not' c.x1)=TRUE & ('not' b.x1)=TRUE;
    hence thesis by A4,MARGREL1:11;
  end;
  suppose
    ('not' c.x1)=TRUE & c.x1=TRUE;
    hence thesis by MARGREL1:11;
  end;
  suppose
    a.x1=TRUE & ('not' b.x1)=TRUE;
    hence thesis by A4,MARGREL1:11;
  end;
  suppose
    a.x1=TRUE & c.x1=TRUE;
    then (a '&' b).x1 =TRUE '&' TRUE by A4,MARGREL1:def 20
      .=TRUE;
    then B_SUP(a '&' b,CompF(PA,G)).z = TRUE by A3,BVFUNC_1:def 17;
    hence thesis by BVFUNC_2:def 10;
  end;
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
  (Ex(c,PA,G) '&' All(b 'imp' 'not' c,PA,G) '&' All(c 'imp' a,PA,G)).z =TRUE;
  then
A1: (Ex(c,PA,G) '&' All(b 'imp' 'not' c,PA,G)).z '&' All(c 'imp' a,PA,G).z=
  TRUE by MARGREL1:def 20;
  then
  Ex(c,PA,G).z '&' All(b 'imp' 'not' c,PA,G).z '&' All(c 'imp' a,PA,G).z=
  TRUE by MARGREL1:def 20;
  then
A2: Ex(c,PA,G).z '&' All(b 'imp' 'not' c,PA,G).z=TRUE by MARGREL1:12;
  now
    assume
    not (ex x being Element of Y st x in EqClass(z,CompF(PA,G)) & c.x= TRUE);
    then B_SUP(c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 17;
    then Ex(c,PA,G).z=FALSE by BVFUNC_2:def 10;
    hence contradiction by A2,MARGREL1:12;
  end;
  then consider x1 being Element of Y such that
A3: x1 in EqClass(z,CompF(PA,G)) and
A4: c.x1=TRUE;
A5: ('not' c.x1)=TRUE or ('not' c.x1)=FALSE by XBOOLEAN:def 3;
  now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
    holds (c 'imp' a).x=TRUE);
    then B_INF(c 'imp' a,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(c 'imp' a,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A1,MARGREL1:12;
  end;
  then (c 'imp' a).x1=TRUE by A3;
  then
A6: ('not' c.x1) 'or' a.x1=TRUE by BVFUNC_1:def 8;
A7: ('not' b.x1)=TRUE or ('not' b.x1)=FALSE by XBOOLEAN:def 3;
  now
    assume not (for x being Element of Y st x in EqClass(z,CompF(PA,G))
    holds (b 'imp' 'not' c).x=TRUE);
    then B_INF(b 'imp' 'not' c,CompF(PA,G)).z = FALSE by BVFUNC_1:def 16;
    then All(b 'imp' 'not' c,PA,G).z=FALSE by BVFUNC_2:def 9;
    hence contradiction by A2,MARGREL1:12;
  end;
  then (b 'imp' 'not' c).x1=TRUE by A3;
  then
A8: ('not' b.x1) 'or' ('not' c).x1=TRUE by BVFUNC_1:def 8;
  per cases by A6,A5,A8,A7,BINARITH:3;
  suppose
    ('not' c.x1)=TRUE & ('not' b.x1)=TRUE;
    hence thesis by A4,MARGREL1:11;
  end;
  suppose
    ('not' c.x1)=TRUE & ('not' c).x1=TRUE;
    hence thesis by A4,MARGREL1:11;
  end;
  suppose
A9: a.x1=TRUE & ('not' b.x1)=TRUE;
    (a '&' 'not' b).x1 =a.x1 '&' ('not' b).x1 by MARGREL1:def 20
      .=TRUE '&' TRUE by A9,MARGREL1:def 19
      .=TRUE;
    then B_SUP(a '&' 'not' b,CompF(PA,G)).z=TRUE by A3,BVFUNC_1:def 17;
    hence thesis by BVFUNC_2:def 10;
  end;
  suppose
    a.x1=TRUE & ('not' c).x1=TRUE;
    then 'not' c.x1=TRUE by MARGREL1:def 19;
    hence thesis by A4,MARGREL1:11;
  end;
end;