:: Propositional Calculus for Boolean Valued Functions, { V }
::  by Shunichi Kobayashi
::
:: Received May 5, 1999
:: Copyright (c) 1999-2012 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, FUNCT_2, MARGREL1, XBOOLEAN, PARTIT1,
      FUNCT_1, BVFUNC_1;
 notations XBOOLE_0, SUBSET_1, XBOOLEAN, MARGREL1, FUNCT_2, BVFUNC_1;
 constructors BINARITH, BVFUNC_1;
 registrations XBOOLE_0, XBOOLEAN, MARGREL1;
 requirements ARITHM, BOOLE;
 definitions BVFUNC_1, XBOOLEAN;
 theorems MARGREL1, BVFUNC_1, BVFUNC_4, BVFUNC_5, BVFUNC_6, BVFUNC_7, XBOOLEAN;

begin :: Chap. 1  Propositional Calculus

reserve Y for non empty set,
  a,b,c,d,e,f,g for Function of Y,BOOLEAN;

Lm1: a '&' b '<' a
proof
  let x be Element of Y;
  assume (a '&' b).x = TRUE;
  then a.x '&' b.x = TRUE by MARGREL1:def 20;
  hence thesis by MARGREL1:12;
end;

Lm2: a '&' b '&' c '<' a & a '&' b '&' c '<' b
proof
  a '&' b '&' c = c '&' b '&' a & c '&' b '&' a 'imp' a = I_el(Y) by BVFUNC_1:4
,BVFUNC_6:38;
  hence a '&' b '&' c '<' a by BVFUNC_1:16;
  a '&' b '&' c = a '&' c '&' b & a '&' c '&' b 'imp' b = I_el(Y) by BVFUNC_1:4
,BVFUNC_6:38;
  hence thesis by BVFUNC_1:16;
end;

Lm3: a '&' b '&' c '&' d '<' a & a '&' b '&' c '&' d '<' b
proof
A1: d '&' c '&' b '&' a 'imp' a = I_el(Y) by BVFUNC_6:38;
  a '&' b '&' c '&' d = d '&' c '&' (b '&' a) by BVFUNC_1:4
    .=d '&' c '&' b '&' a by BVFUNC_1:4;
  hence a '&' b '&' c '&' d '<' a by A1,BVFUNC_1:16;
A2: a '&' c '&' d '&' b 'imp' b = I_el(Y) by BVFUNC_6:38;
  a '&' b '&' c '&' d = a '&' c '&' b '&' d by BVFUNC_1:4
    .=a '&' c '&' d '&' b by BVFUNC_1:4;
  hence thesis by A2,BVFUNC_1:16;
end;

Lm4: a '&' b '&' c '&' d '&' e '<' a & a '&' b '&' c '&' d '&' e '<' b
proof
A1: e '&' d '&' c '&' b '&' a 'imp' a = I_el(Y) by BVFUNC_6:38;
  a '&' b '&' c '&' d '&' e =e '&' d '&' (c '&' (b '&' a)) by BVFUNC_1:4
    .=e '&' d '&' c '&' (b '&' a) by BVFUNC_1:4
    .=e '&' d '&' c '&' b '&' a by BVFUNC_1:4;
  hence a '&' b '&' c '&' d '&' e '<' a by A1,BVFUNC_1:16;
A2: a '&' c '&' d '&' e '&' b 'imp' b = I_el(Y) by BVFUNC_6:38;
  a '&' b '&' c '&' d '&' e =a '&' c '&' b '&' d '&' e by BVFUNC_1:4
    .=a '&' c '&' d '&' b '&' e by BVFUNC_1:4
    .=a '&' c '&' d '&' e '&' b by BVFUNC_1:4;
  hence thesis by A2,BVFUNC_1:16;
end;

Lm5: a '&' b '&' c '&' d '&' e '&' f '<' a & a '&' b '&' c '&' d '&' e '&' f
'<' b
proof
A1: f '&' e '&' d '&' c '&' b '&' a 'imp' a = I_el(Y) by BVFUNC_6:38;
  a '&' b '&' c '&' d '&' e '&' f =f '&' e '&' (d '&' (c '&' (b '&' a)))
  by BVFUNC_1:4
    .=f '&' e '&' d '&' (c '&' (b '&' a)) by BVFUNC_1:4
    .=f '&' e '&' d '&' c '&' (b '&' a) by BVFUNC_1:4
    .=f '&' e '&' d '&' c '&' b '&' a by BVFUNC_1:4;
  hence a '&' b '&' c '&' d '&' e '&' f '<' a by A1,BVFUNC_1:16;
A2: f '&' e '&' d '&' c '&' a '&' b 'imp' b = I_el(Y) by BVFUNC_6:38;
  a '&' b '&' c '&' d '&' e '&' f =f '&' e '&' (d '&' (c '&' (b '&' a)))
  by BVFUNC_1:4
    .=f '&' e '&' d '&' (c '&' (b '&' a)) by BVFUNC_1:4
    .=f '&' e '&' d '&' c '&' (b '&' a) by BVFUNC_1:4
    .=f '&' e '&' d '&' c '&' a '&' b by BVFUNC_1:4;
  hence thesis by A2,BVFUNC_1:16;
end;

Lm6: a '&' b '&' c '&' d '&' e '&' f '&' g '<' a & a '&' b '&' c '&' d '&' e
'&' f '&' g '<' b
proof
A1: g '&' f '&' e '&' d '&' c '&' b '&' a 'imp' a = I_el(Y) by BVFUNC_6:38;
  a '&' b '&' c '&' d '&' e '&' f '&' g =g '&' f '&' (e '&' (d '&' (c '&'
  (b '&' a)))) by BVFUNC_1:4
    .=g '&' f '&' e '&' (d '&' (c '&' (b '&' a))) by BVFUNC_1:4
    .=g '&' f '&' e '&' d '&' (c '&' (b '&' a)) by BVFUNC_1:4
    .=g '&' f '&' e '&' d '&' c '&' (b '&' a) by BVFUNC_1:4
    .=g '&' f '&' e '&' d '&' c '&' b '&' a by BVFUNC_1:4;
  hence a '&' b '&' c '&' d '&' e '&' f '&' g '<' a by A1,BVFUNC_1:16;
A2: a '&' g '&' f '&' e '&' d '&' c '&' b 'imp' b = I_el(Y) by BVFUNC_6:38;
  a '&' b '&' c '&' d '&' e '&' f '&' g =a '&' (c '&' b) '&' d '&' e '&' f
  '&' g by BVFUNC_1:4
    .=a '&' (d '&' (c '&' b)) '&' e '&' f '&' g by BVFUNC_1:4
    .=a '&' (e '&' (d '&' (c '&' b))) '&' f '&' g by BVFUNC_1:4
    .=a '&' (f '&' (e '&' (d '&' (c '&' b)))) '&' g by BVFUNC_1:4
    .=a '&' g '&' (f '&' (e '&' (d '&' (c '&' b)))) by BVFUNC_1:4
    .=a '&' g '&' f '&' (e '&' (d '&' (c '&' b))) by BVFUNC_1:4
    .=a '&' g '&' f '&' e '&' (d '&' (c '&' b)) by BVFUNC_1:4
    .=a '&' g '&' f '&' e '&' d '&' (c '&' b) by BVFUNC_1:4
    .=a '&' g '&' f '&' e '&' d '&' c '&' b by BVFUNC_1:4;
  hence thesis by A2,BVFUNC_1:16;
end;

theorem Th1:
  (a 'or' b) '&' (b 'imp' c) '<' a 'or' c
proof
  let z be Element of Y;
A1: ((a 'or' b) '&' (b 'imp' c)).z =(a 'or' b).z '&' (b 'imp' c).z by
MARGREL1:def 20
    .=(a 'or' b).z '&' ('not' b 'or' c).z by BVFUNC_4:8
    .=(a 'or' b).z '&' (('not' b).z 'or' c.z) by BVFUNC_1:def 4
    .=(a.z 'or' b.z) '&' (('not' b).z 'or' c.z) by BVFUNC_1:def 4;
  assume
A2: ((a 'or' b) '&' (b 'imp' c)).z=TRUE;
  now
    assume (a 'or' c).z<>TRUE;
    then (a 'or' c).z=FALSE by XBOOLEAN:def 3;
    then
A3: a.z 'or' c.z=FALSE by BVFUNC_1:def 4;
    c.z=TRUE or c.z=FALSE by XBOOLEAN:def 3;
    then (a.z 'or' b.z) '&' (('not' b).z 'or' c.z) =b.z '&' 'not' b.z by A3,
MARGREL1:def 19
      .=FALSE by XBOOLEAN:138;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem Th2:
  a '&' (a 'imp' b) '<' b
proof
  let z be Element of Y;
A1: (a '&' (a 'imp' b)).z =a.z '&' (a 'imp' b).z by MARGREL1:def 20
    .=a.z '&' ('not' a 'or' b).z by BVFUNC_4:8
    .=a.z '&' (('not' a).z 'or' b.z) by BVFUNC_1:def 4
    .=a.z '&' ('not' a).z 'or' a.z '&' b.z by XBOOLEAN:8
    .=a.z '&' 'not' a.z 'or' a.z '&' b.z by MARGREL1:def 19
    .=FALSE 'or' a.z '&' b.z by XBOOLEAN:138
    .=a.z '&' b.z;
  assume
A2: (a '&' (a 'imp' b)).z=TRUE;
  now
    assume b.z<>TRUE;
    then a.z '&' b.z =FALSE '&' a.z by XBOOLEAN:def 3
      .=FALSE;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  (a 'imp' b) '&' 'not' b '<' 'not' a
proof
  let z be Element of Y;
  reconsider bz = b.z as boolean set;
A1: ((a 'imp' b) '&' 'not' b).z =(a 'imp' b).z '&' ('not' b).z by
MARGREL1:def 20
    .=('not' a 'or' b).z '&' ('not' b).z by BVFUNC_4:8
    .=('not' b).z '&' (('not' a).z 'or' b.z) by BVFUNC_1:def 4
    .=('not' b).z '&' ('not' a).z 'or' ('not' b).z '&' b.z by XBOOLEAN:8
    .=('not' b).z '&' ('not' a).z 'or' 'not' bz '&' bz by MARGREL1:def 19
    .=('not' b).z '&' ('not' a).z 'or' FALSE by XBOOLEAN:138
    .=('not' b).z '&' ('not' a).z;
  assume
A2: ((a 'imp' b) '&' 'not' b).z=TRUE;
  now
    assume ('not' a).z<>TRUE;
    then ('not' b).z '&' ('not' a).z =FALSE '&' ('not' b).z by XBOOLEAN:def 3
      .=FALSE;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  (a 'or' b) '&' 'not' a '<' b
proof
  let z be Element of Y;
  reconsider az = a.z as boolean set;
A1: ((a 'or' b) '&' 'not' a).z =(a 'or' b).z '&' ('not' a).z by MARGREL1:def 20
    .=('not' a).z '&' (a.z 'or' b.z) by BVFUNC_1:def 4
    .=('not' a).z '&' a.z 'or' ('not' a).z '&' b.z by XBOOLEAN:8
    .='not' az '&' az 'or' ('not' a).z '&' b.z by MARGREL1:def 19
    .=FALSE 'or' ('not' a).z '&' b.z by XBOOLEAN:138
    .=('not' a).z '&' b.z;
  assume
A2: ((a 'or' b) '&' 'not' a).z=TRUE;
  now
    assume b.z<>TRUE;
    then ('not' a).z '&' b.z =FALSE '&' ('not' a).z by XBOOLEAN:def 3
      .=FALSE;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  (a 'imp' b) '&' ('not' a 'imp' b) '<' b
proof
  let z be Element of Y;
  reconsider az = a.z as boolean set;
A1: ((a 'imp' b) '&' ('not' a 'imp' b)).z =(a 'imp' b).z '&' ('not' a 'imp'
  b).z by MARGREL1:def 20
    .=('not' a 'or' b).z '&' ('not' a 'imp' b).z by BVFUNC_4:8
    .=('not' a 'or' b).z '&' ('not' 'not' a 'or' b).z by BVFUNC_4:8
    .=(('not' a).z 'or' b.z) '&' (a 'or' b).z by BVFUNC_1:def 4
    .=(('not' a).z 'or' b.z) '&' (a.z 'or' b.z) by BVFUNC_1:def 4;
  assume
A2: ((a 'imp' b) '&' ('not' a 'imp' b)).z=TRUE;
  now
    assume b.z<>TRUE;
    then b.z=FALSE by XBOOLEAN:def 3;
    then (('not' a).z 'or' b.z) '&' (a.z 'or' b.z) ='not' az '&' az by
MARGREL1:def 19
      .=FALSE by XBOOLEAN:138;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  (a 'imp' b) '&' (a 'imp' 'not' b) '<' 'not' a
proof
  let z be Element of Y;
A1: ((a 'imp' b) '&' (a 'imp' 'not' b)).z =(a 'imp' b).z '&' (a 'imp' 'not'
  b).z by MARGREL1:def 20
    .=('not' a 'or' b).z '&' (a 'imp' 'not' b).z by BVFUNC_4:8
    .=('not' a 'or' b).z '&' ('not' a 'or' 'not' b).z by BVFUNC_4:8
    .=(('not' a).z 'or' b.z) '&' ('not' a 'or' 'not' b).z by BVFUNC_1:def 4
    .=(('not' a).z 'or' b.z) '&' (('not' a).z 'or' ('not' b).z) by
BVFUNC_1:def 4;
  assume
A2: ((a 'imp' b) '&' (a 'imp' 'not' b)).z=TRUE;
  now
    assume ('not' a).z<>TRUE;
    then ('not' a).z=FALSE by XBOOLEAN:def 3;
    then (('not' a).z 'or' b.z) '&' (('not' a).z 'or' ('not' b).z) =b.z '&'
    'not' b.z by MARGREL1:def 19
      .=FALSE by XBOOLEAN:138;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  a 'imp' (b '&' c) '<' a 'imp' b
proof
  let z be Element of Y;
A1: (a 'imp' (b '&' c)).z =('not' a 'or' (b '&' c)).z by BVFUNC_4:8
    .=('not' a).z 'or' (b '&' c).z by BVFUNC_1:def 4
    .=('not' a).z 'or' (b.z '&' c.z) by MARGREL1:def 20;
  assume
A2: (a 'imp' (b '&' c)).z=TRUE;
  now
    assume (a 'imp' b).z<>TRUE;
    then (a 'imp' b).z=FALSE by XBOOLEAN:def 3;
    then ('not' a 'or' b).z=FALSE by BVFUNC_4:8;
    then
A3: ('not' a).z 'or' b.z=FALSE by BVFUNC_1:def 4;
    ('not' a).z 'or' (b.z '&' c.z) =(('not' a).z 'or' b.z) '&' (('not' a).
    z 'or' c.z) by XBOOLEAN:9
      .=FALSE by A3;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  (a 'or' b) 'imp' c '<' a 'imp' c
proof
  let z be Element of Y;
A1: ((a 'or' b) 'imp' c).z =('not'( a 'or' b) 'or' c).z by BVFUNC_4:8
    .=(('not' a '&' 'not' b) 'or' c).z by BVFUNC_1:13
    .=('not' a '&' 'not' b).z 'or' c.z by BVFUNC_1:def 4
    .=(('not' a).z '&' ('not' b).z) 'or' c.z by MARGREL1:def 20;
  assume
A2: ((a 'or' b) 'imp' c).z=TRUE;
  now
    assume (a 'imp' c).z<>TRUE;
    then (a 'imp' c).z=FALSE by XBOOLEAN:def 3;
    then ('not' a 'or' c).z=FALSE by BVFUNC_4:8;
    then
A3: ('not' a).z 'or' c.z=FALSE by BVFUNC_1:def 4;
    (('not' a).z '&' ('not' b).z) 'or' c.z =(c.z 'or' ('not' a).z) '&' (c.
    z 'or' ('not' b).z) by XBOOLEAN:9
      .=FALSE by A3;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  a 'imp' b '<' (a '&' c) 'imp' b
proof
  let z be Element of Y;
A1: (a 'imp' b).z =('not' a 'or' b).z by BVFUNC_4:8
    .=('not' a).z 'or' b.z by BVFUNC_1:def 4;
  assume
A2: (a 'imp' b).z=TRUE;
  now
    assume ((a '&' c) 'imp' b).z<>TRUE;
    then ((a '&' c) 'imp' b).z=FALSE by XBOOLEAN:def 3;
    then ('not'( a '&' c) 'or' b).z=FALSE by BVFUNC_4:8;
    then ('not'( a '&' c)).z 'or' b.z=FALSE by BVFUNC_1:def 4;
    then ('not' a 'or' 'not' c) .z 'or' b.z=FALSE by BVFUNC_1:14;
    then (('not' c).z 'or' ('not' a).z) 'or' b.z=FALSE by BVFUNC_1:def 4;
    then ('not' c).z 'or' (('not' a).z 'or' b.z)=FALSE;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  a 'imp' b '<' (a '&' c) 'imp' (b '&' c)
proof
  let z be Element of Y;
A1: (a 'imp' b).z =('not' a 'or' b).z by BVFUNC_4:8
    .=('not' a).z 'or' b.z by BVFUNC_1:def 4;
  assume
A2: (a 'imp' b).z=TRUE;
  now
    assume ((a '&' c) 'imp' (b '&' c)).z<>TRUE;
    then ((a '&' c) 'imp' (b '&' c)).z=FALSE by XBOOLEAN:def 3;
    then ('not'( a '&' c) 'or' (b '&' c)).z=FALSE by BVFUNC_4:8;
    then ('not'( a '&' c)).z 'or' (b '&' c).z=FALSE by BVFUNC_1:def 4;
    then ('not' a 'or' 'not' c) .z 'or' (b '&' c).z=FALSE by BVFUNC_1:14;
    then (('not' c).z 'or' ('not' a).z) 'or' (b '&' c).z=FALSE by
BVFUNC_1:def 4;
    then ('not' c).z 'or' (('not' a).z 'or' (b '&' c).z)=FALSE;
    then
A3: ('not' c).z 'or' (('not' a).z 'or' (b.z '&' c.z))=FALSE by MARGREL1:def 20;
    ('not' c).z 'or' ((('not' a).z 'or' b.z) '&' (('not' a).z 'or' c.z))
    =('not' c).z 'or' c.z 'or' ('not' a).z by A2,A1
      .='not' c.z 'or' c.z 'or' ('not' a).z by MARGREL1:def 19
      .=TRUE 'or' ('not' a).z by XBOOLEAN:102
      .=TRUE;
    hence contradiction by A3,XBOOLEAN:9;
  end;
  hence thesis;
end;

theorem
  a 'imp' b '<' a 'imp' (b 'or' c)
proof
  let z be Element of Y;
A1: (a 'imp' b).z =('not' a 'or' b).z by BVFUNC_4:8
    .=('not' a).z 'or' b.z by BVFUNC_1:def 4;
  assume
A2: (a 'imp' b).z=TRUE;
  now
    assume
A3: (a 'imp' (b 'or' c)).z<>TRUE;
    (a 'imp' (b 'or' c)).z =('not' a 'or' (b 'or' c)).z by BVFUNC_4:8
      .=('not' a).z 'or' (b 'or' c).z by BVFUNC_1:def 4
      .=('not' a).z 'or' (b.z 'or' c.z) by BVFUNC_1:def 4
      .=(('not' a).z 'or' b.z) 'or' c.z
      .=TRUE by A2,A1;
    hence contradiction by A3;
  end;
  hence thesis;
end;

theorem
  a 'imp' b '<' (a 'or' c) 'imp' (b 'or' c)
proof
  let z be Element of Y;
A1: (a 'imp' b).z =('not' a 'or' b).z by BVFUNC_4:8
    .=('not' a).z 'or' b.z by BVFUNC_1:def 4;
  assume
A2: (a 'imp' b).z=TRUE;
  now
    assume
A3: ((a 'or' c) 'imp' (b 'or' c)).z<>TRUE;
    ((a 'or' c) 'imp' (b 'or' c)).z =('not'( a 'or' c) 'or' (b 'or' c)).z
    by BVFUNC_4:8
      .=('not'( a 'or' c)).z 'or' (b 'or' c).z by BVFUNC_1:def 4
      .=('not'( a 'or' c)).z 'or' (b.z 'or' c.z) by BVFUNC_1:def 4
      .=(('not'( a 'or' c)).z 'or' b.z) 'or' c.z
      .=((('not' a '&' 'not' c)).z 'or' b.z) 'or' c.z by BVFUNC_1:13
      .=(b.z 'or' (('not' a).z '&' ('not' c).z)) 'or' c.z by MARGREL1:def 20
      .=((('not' a).z 'or' b.z) '&' (b.z 'or' ('not' c).z)) 'or' c.z by
XBOOLEAN:9
      .=b.z 'or' (('not' c).z 'or' c.z) by A2,A1
      .=b.z 'or' ('not' c.z 'or' c.z) by MARGREL1:def 19
      .=b.z 'or' TRUE by XBOOLEAN:102
      .=TRUE;
    hence contradiction by A3;
  end;
  hence thesis;
end;

theorem
  a '&' b 'or' c '<' a 'or' c
proof
  let z be Element of Y;
A1: (a '&' b 'or' c).z =(a '&' b).z 'or' c.z by BVFUNC_1:def 4
    .=(a.z '&' b.z) 'or' c.z by MARGREL1:def 20;
  assume
A2: (a '&' b 'or' c).z=TRUE;
  now
    assume (a 'or' c).z<>TRUE;
    then (a 'or' c).z=FALSE by XBOOLEAN:def 3;
    then
A3: a.z 'or' c.z=FALSE by BVFUNC_1:def 4;
    (a.z '&' b.z) 'or' c.z =(c.z 'or' a.z) '&' (c.z 'or' b.z) by XBOOLEAN:9
      .=FALSE by A3;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  (a '&' b) 'or' (c '&' d) '<' a 'or' c
proof
  let z be Element of Y;
A1: ((a '&' b) 'or' (c '&' d)).z =(a '&' b).z 'or' (c '&' d).z by
BVFUNC_1:def 4
    .=(a.z '&' b.z) 'or' (c '&' d).z by MARGREL1:def 20
    .=(a.z '&' b.z) 'or' (c.z '&' (d).z) by MARGREL1:def 20;
  assume
A2: ((a '&' b) 'or' (c '&' d)).z=TRUE;
  now
    assume (a 'or' c).z<>TRUE;
    then (a 'or' c).z=FALSE by XBOOLEAN:def 3;
    then
A3: a.z 'or' c.z=FALSE by BVFUNC_1:def 4;
    (a.z '&' b.z) 'or' (c.z '&' (d).z) =(c.z 'or' (a.z '&' b.z)) '&' ((a.z
    '&' b.z) 'or' (d).z) by XBOOLEAN:9
      .=((a.z 'or' c.z) '&' (c.z 'or' b.z)) '&' ((a.z '&' b.z) 'or' (d).z)
    by XBOOLEAN:9
      .=FALSE by A3;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  (a 'or' b) '&' (b 'imp' c) '<' a 'or' c by Th1;

theorem
  (a 'imp' b) '&' ('not' a 'imp' c) '<' b 'or' c
proof
  let z be Element of Y;
A1: ((a 'imp' b) '&' ('not' a 'imp' c)).z =(('not' a 'or' b) '&' ('not' a
  'imp' c)).z by BVFUNC_4:8
    .=(('not' a 'or' b) '&' ('not' 'not' a 'or' c)).z by BVFUNC_4:8
    .=('not' a 'or' b).z '&' (a 'or' c).z by MARGREL1:def 20
    .=(('not' a).z 'or' b.z) '&' (a 'or' c).z by BVFUNC_1:def 4
    .=(('not' a).z 'or' b.z) '&' (a.z 'or' c.z) by BVFUNC_1:def 4;
  assume
A2: ((a 'imp' b) '&' ('not' a 'imp' c)).z=TRUE;
  now
    reconsider az = a.z as boolean set;
    assume (b 'or' c).z<>TRUE;
    then (b 'or' c).z=FALSE by XBOOLEAN:def 3;
    then
A3: b.z 'or' c.z=FALSE by BVFUNC_1:def 4;
    c.z=TRUE or c.z=FALSE by XBOOLEAN:def 3;
    then (('not' a).z 'or' b.z) '&' (a.z 'or' c.z) ='not' az '&' az by A3,
MARGREL1:def 19
      .=FALSE by XBOOLEAN:138;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  (a 'imp' c) '&' (b 'imp' 'not' c) '<' 'not' a 'or' 'not' b
proof
  let z be Element of Y;
A1: ((a 'imp' c) '&' (b 'imp' 'not' c)).z =(a 'imp' c).z '&' (b 'imp' 'not'
  c).z by MARGREL1:def 20
    .=('not' a 'or' c).z '&' (b 'imp' 'not' c).z by BVFUNC_4:8
    .=('not' a 'or' c).z '&' ('not' b 'or' 'not' c).z by BVFUNC_4:8
    .=(('not' a).z 'or' c.z) '&' ('not' b 'or' 'not' c).z by BVFUNC_1:def 4
    .=(('not' a).z 'or' c.z) '&' (('not' b).z 'or' ('not' c).z) by
BVFUNC_1:def 4;
  assume
A2: ((a 'imp' c) '&' (b 'imp' 'not' c)).z=TRUE;
  now
    assume ('not' a 'or' 'not' b).z<>TRUE;
    then ('not' a 'or' 'not' b).z=FALSE by XBOOLEAN:def 3;
    then
A3: ('not' a).z 'or' ('not' b).z=FALSE by BVFUNC_1:def 4;
    ('not' b).z=TRUE or ('not' b).z=FALSE by XBOOLEAN:def 3;
    then (('not' a).z 'or' c.z) '&' (('not' b).z 'or' ('not' c).z) =c.z '&'
    'not' c.z by A3,MARGREL1:def 19
      .=FALSE by XBOOLEAN:138;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem
  (a 'or' b) '&' ('not' a 'or' c) '<' b 'or' c
proof
  let z be Element of Y;
A1: ((a 'or' b) '&' ('not' a 'or' c)).z =(a 'or' b).z '&' ('not' a 'or' c).z
  by MARGREL1:def 20
    .=(a.z 'or' b.z) '&' ('not' a 'or' c).z by BVFUNC_1:def 4
    .=(a.z 'or' b.z) '&' (('not' a).z 'or' c.z) by BVFUNC_1:def 4;
  assume
A2: ((a 'or' b) '&' ('not' a 'or' c)).z=TRUE;
  now
    assume (b 'or' c).z<>TRUE;
    then (b 'or' c).z=FALSE by XBOOLEAN:def 3;
    then
A3: b.z 'or' c.z=FALSE by BVFUNC_1:def 4;
    c.z=TRUE or c.z=FALSE by XBOOLEAN:def 3;
    then (a.z 'or' b.z) '&' (('not' a).z 'or' c.z) =a.z '&' 'not' a.z by A3,
MARGREL1:def 19
      .=FALSE by XBOOLEAN:138;
    hence contradiction by A2,A1;
  end;
  hence thesis;
end;

theorem Th19:
  (a 'imp' b) '&' (c 'imp' d) '<' (a '&' c) 'imp' (b '&' d)
proof
  let z be Element of Y;
A1: ((a 'imp' b) '&' (c 'imp' d)).z =(a 'imp' b).z '&' (c 'imp' d).z by
MARGREL1:def 20
    .=('not' a 'or' b).z '&' (c 'imp' d).z by BVFUNC_4:8
    .=('not' a 'or' b).z '&' ('not' c 'or' d).z by BVFUNC_4:8
    .=(('not' a).z 'or' b.z) '&' ('not' c 'or' d).z by BVFUNC_1:def 4
    .=(('not' a).z 'or' b.z) '&' (('not' c).z 'or' (d).z) by BVFUNC_1:def 4;
  assume
A2: ((a 'imp' b) '&' (c 'imp' d)).z=TRUE;
  now
A3: ('not' c).z=TRUE or ('not' c).z=FALSE by XBOOLEAN:def 3;
A4: (('not' a).z 'or' ('not' c).z)=TRUE or (('not' a).z 'or' ('not' c).z)=
    FALSE by XBOOLEAN:def 3;
A5: (b.z '&' (d).z)=TRUE or (b.z '&' (d).z)=FALSE by XBOOLEAN:def 3;
A6: ((a '&' c) 'imp' (b '&' d)).z =('not'( a '&' c) 'or' (b '&' d)).z by
BVFUNC_4:8
      .=('not'( a '&' c)).z 'or' (b '&' d).z by BVFUNC_1:def 4
      .=('not' a 'or' 'not' c).z 'or' (b '&' d).z by BVFUNC_1:14
      .=(('not' a).z 'or' ('not' c).z) 'or' (b '&' d).z by BVFUNC_1:def 4
      .=(('not' a).z 'or' ('not' c).z) 'or' (b.z '&' (d).z) by MARGREL1:def 20;
    assume
A7: ((a '&' c) 'imp' (b '&' d)).z<>TRUE;
    now
      per cases by A7,A6,A5,MARGREL1:12;
      case
        b.z=FALSE;
        thus thesis by A2,A1,A6,A4,A3;
      end;
      case
        (d).z=FALSE;
        thus thesis by A2,A1,A6,A4,A3;
      end;
    end;
    hence thesis;
  end;
  hence thesis;
end;

theorem
  (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b '&' c)
proof
  (a 'imp' b) '&' (a 'imp' c) '<' (a '&' a) 'imp' (b '&' c) by Th19;
  hence thesis;
end;

theorem Th21:
  ((a 'imp' c) '&' (b 'imp' c)) '<' (a 'or' b) 'imp' c
proof
  ((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c) = I_el Y by
BVFUNC_6:9;
  hence thesis by BVFUNC_1:16;
end;

theorem Th22:
  (a 'imp' b) '&' (c 'imp' d) '<' (a 'or' c) 'imp' (b 'or' d)
proof
  let z be Element of Y;
A1: ((a 'imp' b) '&' (c 'imp' d)).z =(('not' a 'or' b) '&' (c 'imp' d)).z by
BVFUNC_4:8
    .=(('not' a 'or' b) '&' ('not' c 'or' d)).z by BVFUNC_4:8
    .=('not' a 'or' b).z '&' ('not' c 'or' d).z by MARGREL1:def 20
    .=(('not' a).z 'or' b.z) '&' ('not' c 'or' d).z by BVFUNC_1:def 4
    .=(('not' a).z 'or' b.z) '&' (('not' c).z 'or' (d).z) by BVFUNC_1:def 4;
  assume
A2: ((a 'imp' b) '&' (c 'imp' d)).z=TRUE;
  now
A3: (d).z=TRUE or (d).z=FALSE by XBOOLEAN:def 3;
A4: (b.z 'or' (d).z)=TRUE or (b.z 'or' (d).z)=FALSE by XBOOLEAN:def 3;
A5: (('not' a).z '&' ('not' c).z)=TRUE or (('not' a).z '&' ('not' c).z)=
    FALSE by XBOOLEAN:def 3;
A6: ((a 'or' c) 'imp' (b 'or' d)).z =('not'( a 'or' c) 'or' (b 'or' d)).z
    by BVFUNC_4:8
      .=(('not' a '&' 'not' c) 'or' (b 'or' d)).z by BVFUNC_1:13
      .=('not' a '&' 'not' c).z 'or' (b 'or' d).z by BVFUNC_1:def 4
      .=(('not' a).z '&' ('not' c).z) 'or' (b 'or' d).z by MARGREL1:def 20
      .=(('not' a).z '&' ('not' c).z) 'or' (b.z 'or' (d).z) by BVFUNC_1:def 4;
    assume
A7: ((a 'or' c) 'imp' (b 'or' d)).z<>TRUE;
    now
      per cases by A7,A6,A5,MARGREL1:12;
      case
        ('not' a).z=FALSE;
        thus thesis by A2,A1,A6,A4,A3;
      end;
      case
        ('not' c).z=FALSE;
        thus thesis by A2,A1,A6,A4,A3;
      end;
    end;
    hence thesis;
  end;
  hence thesis;
end;

theorem
  (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b 'or' c)
proof
  (a 'imp' b) '&' (a 'imp' c) '<' (a 'or' a) 'imp' (b 'or' c) by Th22;
  hence thesis;
end;

theorem Th24:
  for a1,b1,c1,a2,b2,c2 being Function of Y,BOOLEAN holds (
  b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2)
  '&' 'not'( a2 '&' c2) '<' (a2 'imp' a1)
proof
  let a1,b1,c1,a2,b2,c2 be Function of Y,BOOLEAN;
A1: ((b1 'or' c1) 'imp' (b2 'or' c2)) '&' ((b2 'or' c2) 'imp' 'not' a2) '&'
((b1 'or' c1) 'imp' 'not' a2) 'imp' ((b1 'or' c1) 'imp' 'not' a2) = I_el(Y) by
BVFUNC_6:38;
A2: (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( a2 '&' c2) 'imp' (c1 'imp' c2) = I_el(Y)
     by BVFUNC_1:16,Lm4;
A3: ((b1 'imp' b2) '&' (c1 'imp' c2)) 'imp' ((b1 'or' c1) 'imp' (b2 'or' c2
  )) = I_el(Y) by BVFUNC_1:16,Th22;
  (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( a2 '&' c2) 'imp' (b1 'imp' b2) = I_el(Y)
          by BVFUNC_1:16,Lm4;
  then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( a2 '&' c2) 'imp' (b1 'imp' b2) '&' (c1 'imp' c2) = I_el(Y)
  by A2,BVFUNC_6:18;
  then
A4: (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
'&' b2) '&' 'not'( a2 '&' c2) 'imp' ((b1 'or' c1) 'imp' (b2 'or' c2)) = I_el(Y)
  by A3,BVFUNC_5:9;
A5: (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( a2 '&' c2) 'imp' 'not'( a2 '&' c2) = I_el(Y) by
BVFUNC_1:16,Lm1;
  (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( a2 '&' c2) 'imp' 'not'( a2 '&' b2) = I_el(Y) by
BVFUNC_1:16,Lm2;
  then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
'&' b2) '&' 'not'( a2 '&' c2) 'imp' ('not'( a2 '&' b2) '&' 'not'( a2 '&' c2)) =
  I_el(Y) by A5,BVFUNC_6:18;
  then
A6: (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( a2 '&' c2) 'imp' ((b1 'or' c1) 'imp' (b2 'or' c2)) '&' (
  'not'( a2 '&' b2) '&' 'not' (a2 '&' c2)) = I_el(Y) by A4,BVFUNC_6:18;
  'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) =('not' a2 'or' 'not' b2) '&'
  'not'( a2 '&' c2) by BVFUNC_1:14
    .=('not' b2 'or' 'not' a2) '&' ('not' c2 'or' 'not' a2) by BVFUNC_1:14
    .=(b2 'imp' 'not' a2) '&' ('not' c2 'or' 'not' a2) by BVFUNC_4:8
    .=(b2 'imp' 'not' a2) '&' (c2 'imp' 'not' a2) by BVFUNC_4:8
    .=(b2 'or' c2) 'imp' 'not' a2 by BVFUNC_7:5;
  then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
'&' b2) '&' 'not'( a2 '&' c2) 'imp' ((b1 'or' c1) 'imp' (b2 'or' c2)) '&' ((b2
  'or' c2) 'imp' 'not' a2) '&' ((b1 'or' c1) 'imp' 'not' a2) = I_el(Y) by A6,
BVFUNC_7:12;
  then
A7: (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
'&' b2) '&' 'not'( a2 '&' c2) 'imp' ((b1 'or' c1) 'imp' 'not' a2) = I_el(Y) by
A1,BVFUNC_5:9;
  (a1 'or' b1 'or' c1) '&' ((b1 'or' c1) 'imp' 'not' a2) =(a1 'or' (b1
'or' c1) ) '&' ((b1 'or' c1) 'imp' 'not' a2) & (a1 'or' (b1 'or' c1)) '&' ((b1
  'or' c1) 'imp' 'not' a2) '<' (a1 'or' 'not' a2) by Th1,BVFUNC_1:8;
  then
A8: (a1 'or' b1 'or' c1) '&' ((b1 'or' c1) 'imp' 'not' a2) 'imp' (a1 'or'
  'not' a2) =I_el(Y) by BVFUNC_1:16;
  (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( a2 '&' c2) 'imp' (a1 'or' b1 'or' c1) = I_el(Y) by
BVFUNC_1:16,Lm3;
  then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( a2 '&' c2) 'imp' (a1 'or' b1 'or' c1) '&' ((b1 'or' c1)
  'imp' 'not' a2) = I_el(Y) by A7,BVFUNC_6:18;
  then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( a2 '&' c2) 'imp' (a1 'or' 'not' a2) = I_el(Y) by A8,
BVFUNC_5:9;
  then (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( a2 '&' c2) 'imp' (a2 'imp' a1) = I_el(Y) by BVFUNC_4:8;
  hence thesis by BVFUNC_1:16;
end;

Lm8: for a1,b1,c1,a2,b2,c2 being Function of Y,BOOLEAN holds ((a1 'imp'
a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
'&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' ((a1 'imp' a2) '&' (
b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&' 'not'( c2 '&' a2) '&' 'not'( c2 '&'
b2)) =I_el(Y)
proof
  let a1,b1,c1,a2,b2,c2 be Function of Y,BOOLEAN;
A1: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
  c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp'
  'not'( a2 '&' c2) = I_el(Y) by Lm2,BVFUNC_1:16;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
a1 'imp' a2) = I_el(Y) & ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
( a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2
  '&' c2)) 'imp' (b1 'imp' b2) = I_el(Y)
   by Lm6,BVFUNC_1:16;
  then
A2: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
  a1 'imp' a2) '&' (b1 'imp' b2) = I_el(Y) by BVFUNC_6:18;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
  a1 'or' b1 'or' c1) = I_el(Y) by Lm4,BVFUNC_1:16;
  then
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
  a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) = I_el(Y) by A2,
BVFUNC_6:18;
  then
A3: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2 '&' c2) =
  I_el(Y) by A1,BVFUNC_6:18;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
  c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp'
  'not'( b2 '&' c2) = I_el(Y) by Lm1,BVFUNC_1:16;
  hence thesis by A3,BVFUNC_6:18;
end;

Lm9: for a1,b1,c1,a2,b2,c2 being Function of Y,BOOLEAN holds ((a1 'imp'
a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
'&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' ((a1 'imp' a2) '&' (
c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( b2 '&' a2) '&' 'not'( b2 '&'
c2)) = I_el(Y)
proof
  let a1,b1,c1,a2,b2,c2 be Function of Y,BOOLEAN;
A1: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
  c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp'
  'not'( a2 '&' b2) = I_el(Y) by Lm3,BVFUNC_1:16;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
a1 'imp' a2) = I_el(Y) & ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
( a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2
  '&' c2)) 'imp' (c1 'imp' c2) = I_el(Y)
   by Lm5,Lm6,BVFUNC_1:16;
  then
A2: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
  a1 'imp' a2) '&' (c1 'imp' c2) = I_el(Y) by BVFUNC_6:18;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
  a1 'or' b1 'or' c1) = I_el(Y) by Lm4,BVFUNC_1:16;
  then
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
  a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) = I_el(Y) by A2,
BVFUNC_6:18;
  then
A3: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) =
  I_el(Y) by A1,BVFUNC_6:18;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
  c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp'
  'not'( b2 '&' c2) = I_el(Y) by Lm1,BVFUNC_1:16;
  hence thesis by A3,BVFUNC_6:18;
end;

Lm10: for a1,b1,c1,a2,b2,c2 being Function of Y,BOOLEAN holds ((a1 'imp'
a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
'&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' ((b1 'imp' b2) '&' (
c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&'
c2)) =I_el(Y)
proof
  let a1,b1,c1,a2,b2,c2 be Function of Y,BOOLEAN;
A1: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
  c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp'
  'not'( a2 '&' b2) = I_el(Y) by Lm3,BVFUNC_1:16;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
b1 'imp' b2) = I_el(Y) & ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&'
( a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2
  '&' c2)) 'imp' (c1 'imp' c2) = I_el(Y)
    by Lm5,Lm6,BVFUNC_1:16;
  then
A2: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
  b1 'imp' b2) '&' (c1 'imp' c2) = I_el(Y) by BVFUNC_6:18;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
  a1 'or' b1 'or' c1) = I_el(Y) by Lm4,BVFUNC_1:16;
  then
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
  b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) = I_el(Y) by A2,
BVFUNC_6:18;
  then
A3: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) =
  I_el(Y) by A1,BVFUNC_6:18;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
  c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp'
  'not'( a2 '&' c2) = I_el(Y) by Lm2,BVFUNC_1:16;
  hence thesis by A3,BVFUNC_6:18;
end;

theorem
  for a1,b1,c1,a2,b2,c2 being Function of Y,BOOLEAN holds (a1
  'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2) '<' (a2 'imp' a1)
  '&' (b2 'imp' b1) '&' (c2 'imp' c1)
proof
  let a1,b1,c1,a2,b2,c2 be Function of Y,BOOLEAN;
A1: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' ((
  b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2)
  '&' 'not'( a2 '&' c2)) =I_el(Y) by Lm10;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' ((
  a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&' 'not'( c2 '&' a2)
  '&' 'not'( c2 '&' b2)) =I_el(Y) & ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1
'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2)
  '&' 'not'( b2 '&' c2)) 'imp' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1
  'or' c1) '&' 'not'( b2 '&' a2) '&' 'not'( b2 '&' c2)) =I_el(Y) by Lm8,Lm9;
  then
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' ((
  a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&' 'not'( c2 '&' a2)
  '&' 'not'( c2 '&' b2)) '&' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1
  'or' c1) '&' 'not'( b2 '&' a2) '&' 'not'( b2 '&' c2)) =I_el(Y) by BVFUNC_6:18
;
  then
A2: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' ((
  a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&' 'not'( c2 '&' a2)
  '&' 'not'( c2 '&' b2)) '&' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1
'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)) '&' ((b1 'imp' b2) '&' (
  c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&'
  c2)) =I_el(Y) by A1,BVFUNC_6:18;
A3: (a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( b2 '&' c2) 'imp' (b2 'imp' b1) = I_el(Y)
    by BVFUNC_1:16,Th24;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&' 'not'( c2
  '&' a2) '&' 'not'( c2 '&' b2)) '&' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1
'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)) '&' ((b1 'imp' b2
  ) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'(
a2 '&' c2)) 'imp' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&'
  'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)) =I_el(Y)
    by BVFUNC_1:16,Lm2;
  then
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' ((
  a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2)
  '&' 'not'( b2 '&' c2)) =I_el(Y) by A2,BVFUNC_5:9;
  then
A4: (a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2) 'imp' (b2
  'imp' b1) = I_el(Y) by A3,BVFUNC_5:9;
  (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2
  '&' b2) '&' 'not'( a2 '&' c2) 'imp' (a2 'imp' a1) = I_el(Y)
     by BVFUNC_1:16,Th24;
  then (a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not' (b2 '&' c2) 'imp' (a2
  'imp' a1) = I_el(Y) by A1,BVFUNC_5:9;
  then
A5: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
  a2 'imp' a1) '&' (b2 'imp' b1) = I_el(Y) by A4,BVFUNC_6:18;
  (a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' c1 'or' b1) '&' 'not'( c2
  '&' a2) '&' 'not'( c2 '&' b2) '<' (c2 'imp' c1) by Th24;
  then (a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&' 'not'( c2
  '&' a2) '&' 'not'( c2 '&' b2) '<' (c2 'imp' c1) by BVFUNC_1:8;
  then
A6: (a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&' 'not'( c2
  '&' a2) '&' 'not'( c2 '&' b2) 'imp' (c2 'imp' c1) = I_el(Y) by BVFUNC_1:16;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&' 'not'( c2
  '&' a2) '&' 'not'( c2 '&' b2)) '&' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' (a1
'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'( b2 '&' c2)) '&' ((b1 'imp' b2
  ) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or' c1) '&' 'not'( a2 '&' b2) '&' 'not'(
a2 '&' c2)) 'imp' ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&'
  'not'( c2 '&' a2) '&' 'not'( c2 '&' b2)) =I_el(Y) by BVFUNC_1:16,Lm2;
  then
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' ((
  a1 'imp' a2) '&' (b1 'imp' b2) '&' (a1 'or' b1 'or' c1) '&' 'not'( c2 '&' a2)
  '&' 'not'( c2 '&' b2)) =I_el(Y) by A2,BVFUNC_5:9;
  then (a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2) 'imp' (c2
  'imp' c1) = I_el(Y) by A6,BVFUNC_5:9;
  then
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' (a1 'or' b1 'or'
c1) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)) 'imp' (
  a2 'imp' a1) '&' (b2 'imp' b1) '&' (c2 'imp' c1) = I_el(Y) by A5,BVFUNC_6:18;
  hence thesis by BVFUNC_1:16;
end;

theorem Th26:
  for a1,b1,a2,b2 being Function of Y,BOOLEAN holds ((a1
'imp' a2) '&' (b1 'imp' b2) '&' 'not'(a2 '&' b2)) 'imp' 'not' (a1 '&' b1)=I_el(
  Y)
proof
  let a1,b1,a2,b2 be Function of Y,BOOLEAN;
  for z being Element of Y st ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'(
  a2 '&' b2)).z=TRUE holds ('not'( a1 '&' b1)).z=TRUE
  proof
    let z be Element of Y;
A1: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)).z =((a1 'imp'
    a2) '&' (b1 'imp' b2)).z '&' ('not'( a2 '&' b2)).z by MARGREL1:def 20
      .=((a1 'imp' a2).z '&' (b1 'imp' b2).z) '&' ('not'( a2 '&' b2)).z by
MARGREL1:def 20
      .=(('not' a1 'or' a2).z '&' (b1 'imp' b2).z) '&' ('not'( a2 '&' b2)).z
    by BVFUNC_4:8
      .=(('not' a1 'or' a2).z '&' ('not' b1 'or' b2).z) '&' ('not' (a2 '&'
    b2)).z by BVFUNC_4:8
      .=((('not' a1).z 'or' (a2).z) '&' ('not' b1 'or' b2).z) '&' ('not'( a2
    '&' b2)).z by BVFUNC_1:def 4
      .=((('not' a1).z 'or' (a2).z) '&' (('not' b1).z 'or' (b2).z)) '&' (
    'not'( a2 '&' b2)).z by BVFUNC_1:def 4
      .=((('not' a1).z 'or' (a2).z) '&' (('not' b1).z 'or' (b2).z)) '&' ((
    'not' a2 'or' 'not' b2).z) by BVFUNC_1:14
      .=((('not' a1).z 'or' (a2).z) '&' (('not' b1).z 'or' (b2).z)) '&' ((
    'not' a2).z 'or' ('not' b2).z) by BVFUNC_1:def 4;
    assume
A2: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)).z=TRUE;
    now
A3:   ('not' b1).z=TRUE or ('not' b1).z=FALSE by XBOOLEAN:def 3;
A4:   ('not' a1).z=TRUE or ('not' a1).z=FALSE by XBOOLEAN:def 3;
A5:   ('not'( a1 '&' b1)).z =('not' a1 'or' 'not' b1).z by BVFUNC_1:14
        .=('not' a1).z 'or' ('not' b1).z by BVFUNC_1:def 4;
      assume ('not'( a1 '&' b1)).z<>TRUE;
      then ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)).z =((b2).z
'&' (a2).z) '&' ('not' a2).z 'or' ((a2).z '&' (b2).z) '&' ('not' b2).z by A1,A5
,A4,A3,XBOOLEAN:8
        .=(b2).z '&' ((a2).z '&' ('not' a2).z) 'or' (a2).z '&' ((b2).z '&' (
      'not' b2).z)
        .=(b2).z '&' ((a2).z '&' 'not' (a2).z) 'or' (a2).z '&' ((b2).z '&' (
      'not' b2).z) by MARGREL1:def 19
        .=(b2).z '&' ((a2).z '&' 'not' (a2).z) 'or' (a2).z '&' ((b2).z '&'
      'not' (b2).z) by MARGREL1:def 19
        .=(b2).z '&' FALSE 'or' (a2).z '&' ((b2).z '&' 'not' (b2).z) by
XBOOLEAN:138
        .=FALSE 'or' FALSE '&' (a2).z by XBOOLEAN:138
        .=FALSE;
      hence contradiction by A2;
    end;
    hence thesis;
  end;
 hence thesis by BVFUNC_1:16,def 12;
end;

theorem
  for a1,b1,c1,a2,b2,c2 being Function of Y,BOOLEAN holds (a1
'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' b2) '&' 'not'(
  a2 '&' c2) '&' 'not'( b2 '&' c2) '<' 'not'( a1 '&' b1) '&' 'not'( a1 '&' c1)
  '&' 'not'( b1 '&' c1)
proof
  let a1,b1,c1,a2,b2,c2 be Function of Y,BOOLEAN;
A1: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1 'imp'
  a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&' ((b1 'imp' b2) '&' (c1 'imp'
c2) '&' 'not'( b2 '&' c2)) 'imp' ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2
  '&' b2)) '&' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) =I_el(Y)
  by BVFUNC_6:38;
A2: ((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) 'imp' 'not'( a1
  '&' c1)=I_el(Y) by Th26;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1 'imp'
a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) 'imp' ((a1 'imp' a2) '&' (c1 'imp'
  c2) '&' 'not'( a2 '&' c2)) =I_el(Y) by BVFUNC_6:38;
  then ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1 'imp'
  a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&' ((b1 'imp' b2) '&' (c1 'imp'
c2) '&' 'not'( b2 '&' c2)) 'imp' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2
  '&' c2)) =I_el(Y) by A1,BVFUNC_5:9;
  then
A3: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1 'imp'
  a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&' ((b1 'imp' b2) '&' (c1 'imp'
  c2) '&' 'not'( b2 '&' c2)) 'imp' 'not'( a1 '&' c1)=I_el(Y) by A2,BVFUNC_5:9;
A4: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) 'imp' 'not'( a1
  '&' b1)=I_el(Y) by Th26;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1 'imp'
  a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&' ((b1 'imp' b2) '&' (c1 'imp'
c2) '&' 'not'( b2 '&' c2)) 'imp' ((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2
  '&' c2)) =I_el(Y) & ((b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2))
  'imp' 'not'( b1 '&' c1)=I_el(Y) by Th26,BVFUNC_6:38;
  then
A5: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1 'imp'
  a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&' ((b1 'imp' b2) '&' (c1 'imp'
  c2) '&' 'not'( b2 '&' c2)) 'imp' 'not'( b1 '&' c1)=I_el(Y) by BVFUNC_5:9;
  ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1 'imp'
a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) 'imp' ((a1 'imp' a2) '&' (b1 'imp'
  b2) '&' 'not'( a2 '&' b2)) =I_el(Y) by BVFUNC_6:38;
  then ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1 'imp'
  a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&' ((b1 'imp' b2) '&' (c1 'imp'
c2) '&' 'not'( b2 '&' c2)) 'imp' ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2
  '&' b2)) =I_el(Y) by A1,BVFUNC_5:9;
  then ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1 'imp'
  a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&' ((b1 'imp' b2) '&' (c1 'imp'
  c2) '&' 'not'( b2 '&' c2)) 'imp' 'not'( a1 '&' b1)=I_el(Y) by A4,BVFUNC_5:9;
  then ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1 'imp'
  a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&' ((b1 'imp' b2) '&' (c1 'imp'
c2) '&' 'not'( b2 '&' c2)) 'imp' 'not'( a1 '&' b1) '&' 'not'( a1 '&' c1) =I_el(
  Y) by A3,BVFUNC_6:18;
  then
A6: ((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1 'imp'
  a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&' ((b1 'imp' b2) '&' (c1 'imp'
  c2) '&' 'not'( b2 '&' c2)) 'imp' 'not'( a1 '&' b1) '&' 'not'( a1 '&' c1) '&'
  'not'( b1 '&' c1) =I_el(Y) by A5,BVFUNC_6:18;
  (a1 'imp' a2) '&' (b1 'imp' b2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' b2)
  '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2) =(a1 'imp' a2) '&' (a1 'imp' a2)
  '&' ((b1 'imp' b2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2) '&' 'not'( a2 '&' b2)
  '&' 'not'( a2 '&' c2) '&' 'not'( b2 '&' c2)
    .=(((a1 'imp' a2) '&' (a1 'imp' a2) '&' (b1 'imp' b2)) '&' (b1 'imp' b2)
'&' ((c1 'imp' c2) '&' (c1 'imp' c2))) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&'
  c2) '&' 'not'( b2 '&' c2) by BVFUNC_1:4
    .=((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (a1 'imp' a2)) '&' (b1 'imp'
b2) '&' ((c1 'imp' c2) '&' (c1 'imp' c2))) '&' 'not'( a2 '&' b2) '&' 'not'( a2
  '&' c2) '&' 'not'( b2 '&' c2) by BVFUNC_1:4
    .=(((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (a1 'imp' a2) '&' (b1 'imp' b2)
'&' (c1 'imp' c2) '&' (c1 'imp' c2)) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&' c2
  ) '&' 'not'( b2 '&' c2) by BVFUNC_1:4
    .=(((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (a1 'imp' a2) '&' ((b1 'imp' b2
) '&' (c1 'imp' c2)) '&' (c1 'imp' c2)) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&'
  c2) '&' 'not'( b2 '&' c2) by BVFUNC_1:4
    .=(((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((b1 'imp' b2) '&' (c1 'imp' c2
)) '&' (a1 'imp' a2) '&' (c1 'imp' c2)) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&'
  c2) '&' 'not'( b2 '&' c2) by BVFUNC_1:4
    .=((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((b1 'imp' b2) '&' (c1 'imp' c2)
) '&' ((a1 'imp' a2) '&' (c1 'imp' c2)) '&' 'not'( a2 '&' b2) '&' 'not'( a2 '&'
  c2) '&' 'not'( b2 '&' c2) by BVFUNC_1:4
    .=((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((b1 'imp' b2) '&' (c1 'imp' c2)
) '&' ((a1 'imp' a2) '&' (c1 'imp' c2)) '&' 'not'( a2 '&' c2) '&' 'not'( a2 '&'
  b2) '&' 'not'( b2 '&' c2) by BVFUNC_1:4
    .=((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((b1 'imp' b2) '&' (c1 'imp' c2)
) '&' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&' 'not'( a2 '&'
  b2) '&' 'not'( b2 '&' c2) by BVFUNC_1:4
    .=((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((b1 'imp' b2) '&' (c1 'imp' c2)
) '&' 'not'( a2 '&' b2) '&' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not' (a2 '&'
  c2)) '&' 'not'( b2 '&' c2) by BVFUNC_1:4
    .=((a1 'imp' a2) '&' (b1 'imp' b2)) '&' 'not'( a2 '&' b2) '&' ((b1 'imp'
  b2) '&' (c1 'imp' c2)) '&' ((a1 'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&'
  c2)) '&' 'not'( b2 '&' c2) by BVFUNC_1:4
    .=((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((b1 'imp'
  b2) '&' (c1 'imp' c2)) '&' 'not'( b2 '&' c2) '&' ((a1 'imp' a2) '&' (c1 'imp'
  c2) '&' 'not' (a2 '&' c2)) by BVFUNC_1:4
    .=((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((b1 'imp'
  b2) '&' (c1 'imp' c2) '&' 'not'( b2 '&' c2)) '&' ((a1 'imp' a2) '&' (c1 'imp'
  c2) '&' 'not'( a2 '&' c2)) by BVFUNC_1:4
    .=(((a1 'imp' a2) '&' (b1 'imp' b2) '&' 'not'( a2 '&' b2)) '&' ((a1
  'imp' a2) '&' (c1 'imp' c2) '&' 'not'( a2 '&' c2)) '&' ((b1 'imp' b2) '&' (c1
  'imp' c2) '&' 'not'( b2 '&' c2))) by BVFUNC_1:4;
  hence thesis by A6,BVFUNC_1:16;
end;

theorem
  a '&' b '<' a by Lm1;

theorem
  a '&' b '&' c '<' a & a '&' b '&' c '<' b by Lm2;

theorem
  a '&' b '&' c '&' d '<' a & a '&' b '&' c '&' d '<' b by Lm3;

theorem
  a '&' b '&' c '&' d '&' e '<' a & a '&' b '&' c '&' d '&' e '<' b by Lm4;

theorem
  a '&' b '&' c '&' d '&' e '&' f '<' a & a '&' b '&' c '&' d '&' e '&'
  f '<' b by Lm5;

theorem
  a '&' b '&' c '&' d '&' e '&' f '&' g '<' a & a '&' b '&' c '&' d '&'
  e '&' f '&' g '<' b by Lm6;

theorem Th34:
  a '<' b & c '<' d implies a '&' c '<' b '&' d
proof
  assume a '<' b & c '<' d;
  then a 'imp' b = I_el Y & c 'imp' d = I_el Y by BVFUNC_1:16;
  then (a '&' c) 'imp' (b '&' d) = I_el Y by BVFUNC_6:21;
  hence thesis by BVFUNC_1:16;
end;

theorem
  a '&' b '<' c implies a '&' 'not' c '<' 'not' b
proof
  assume a '&' b '<' c;
  then I_el Y = a '&' b 'imp' c by BVFUNC_1:16
    .= 'not' (a '&' b) 'or' c by BVFUNC_4:8
    .= 'not' a 'or' 'not' b 'or' c by BVFUNC_1:14
    .= 'not' a 'or' 'not' 'not' c 'or' 'not' b by BVFUNC_1:8
    .= 'not' (a '&' 'not' c) 'or' 'not' b by BVFUNC_1:14
    .= a '&' 'not' c 'imp' 'not' b by BVFUNC_4:8;
  hence thesis by BVFUNC_1:16;
end;

theorem
  (a 'imp' c) '&' (b 'imp' c) '&' (a 'or' b) '<' c
proof
  set K1 = (a 'imp' c) '&' (b 'imp' c);
  K1 '<' (a 'or' b) 'imp' c by Th21;
  then
A1: K1 '&' (a 'or' b) '<' ((a 'or' b) 'imp' c) '&' (a 'or' b) by Th34;
  ((a 'or' b) 'imp' c) '&' (a 'or' b) '<' c by Th2;
  hence thesis by A1,BVFUNC_1:15;
end;

theorem
  ((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c
proof
  (a 'imp' c) 'or' (b 'imp' c) = (a '&' b) 'imp' c by BVFUNC_7:6;
  hence thesis by Th2;
end;

theorem
  a '<' b & c '<' d implies a 'or' c '<' b 'or' d
proof
  assume a '<' b & c '<' d;
  then a 'imp' b = I_el(Y) & c 'imp' d = I_el(Y) by BVFUNC_1:16;
  then (a 'or' c) 'imp' (b 'or' d) = I_el(Y) by BVFUNC_6:22;
  hence thesis by BVFUNC_1:16;
end;

theorem Th39:
  a '<' a 'or' b
proof
  a 'imp' (a 'or' b) = I_el Y by BVFUNC_6:26;
  hence thesis by BVFUNC_1:16;
end;

theorem
  a '&' b '<' a 'or' b
proof
  a '&' b '<' a & a '<' a 'or' b by Lm1,Th39;
  hence thesis by BVFUNC_1:15;
end;