:: BVFUNC_9 semantic presentation

begin

        Lm1:  for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b '<' a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' b '<' a
let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' b '<' a
let x be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a '&' b) . x = TRUE or a . x = TRUE )
assume  (a '&' b) . x = TRUE ; ::_thesis: a . x = TRUE
then  (a . x) '&' (b . x) = TRUE by MARGREL1:def_20;
hence  a . x = TRUE by MARGREL1:12; ::_thesis: verum
end;

Lm2:  for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds
( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b )
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds
( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b )
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b )
 ( (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; ::_thesis: (a '&' b) '&' c '<' b
 ( (a '&' b) '&' c = (a '&' c) '&' b & ((a '&' c) '&' b) 'imp' b = I_el Y ) by BVFUNC_1:4, BVFUNC_6:38;
hence  (a '&' b) '&' c '<' b by BVFUNC_1:16; ::_thesis: verum
end;

Lm3:  for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds
( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b )
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds
( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b )
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b )
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; ::_thesis: ((a '&' b) '&' c) '&' d '<' b
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  ((a '&' b) '&' c) '&' d '<' b by A2, BVFUNC_1:16; ::_thesis: verum
end;

Lm4:  for Y being non empty set
for a, b, c, d, e being Function of Y,BOOLEAN holds
( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b )
proof
let Y be non empty set ; ::_thesis: for a, b, c, d, e being Function of Y,BOOLEAN holds
( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b )
let a, b, c, d, e be Function of Y,BOOLEAN; ::_thesis: ( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b )
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; ::_thesis: (((a '&' b) '&' c) '&' d) '&' e '<' b
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  (((a '&' b) '&' c) '&' d) '&' e '<' b by A2, BVFUNC_1:16; ::_thesis: verum
end;

Lm5:  for Y being non empty set
for a, b, c, d, e, f being Function of Y,BOOLEAN holds
( ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' a & ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b )
proof
let Y be non empty set ; ::_thesis: for a, b, c, d, e, f being Function of Y,BOOLEAN holds
( ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' a & ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b )
let a, b, c, d, e, f be Function of Y,BOOLEAN; ::_thesis: ( ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' a & ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b )
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; ::_thesis: ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b
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  ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b by A2, BVFUNC_1:16; ::_thesis: verum
end;

Lm6:  for Y being non empty set
for a, b, c, d, e, f, g being Function of Y,BOOLEAN holds
( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b )
proof
let Y be non empty set ; ::_thesis: for a, b, c, d, e, f, g being Function of Y,BOOLEAN holds
( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b )
let a, b, c, d, e, f, g be Function of Y,BOOLEAN; ::_thesis: ( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b )
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; ::_thesis: (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b
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  (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b by A2, BVFUNC_1:16; ::_thesis: verum
end;

theorem Th1: :: BVFUNC_9:1
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (b 'imp' c) '<' a 'or' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (b 'imp' c) '<' a 'or' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) '&' (b 'imp' c) '<' a 'or' c
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'or' b) '&' (b 'imp' c)) . z = TRUE or (a 'or' c) . z = TRUE )
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 ; ::_thesis: (a 'or' c) . z = TRUE
now__::_thesis:_not_(a_'or'_c)_._z_<>_TRUE
assume  (a 'or' c) . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  (a 'or' c) . z = TRUE ; ::_thesis: verum
end;

theorem Th2: :: BVFUNC_9:2
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' (a 'imp' b) '<' b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' (a 'imp' b) '<' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' (a 'imp' b) '<' b
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a '&' (a 'imp' b)) . z = TRUE or b . z = TRUE )
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 ; ::_thesis: b . z = TRUE
now__::_thesis:_not_b_._z_<>_TRUE
assume  b . z <> TRUE ; ::_thesis: contradiction
then (a . z) '&' (b . z) = FALSE '&' (a . z) by XBOOLEAN:def_3
.= FALSE ;
hence  contradiction by A2, A1; ::_thesis: verum
end;
hence  b . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:3
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' ('not' b) '<' 'not' a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' ('not' b) '<' 'not' a
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' ('not' b) '<' 'not' a
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' ('not' b)) . z = TRUE or ('not' a) . z = TRUE )
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 ; ::_thesis: ('not' a) . z = TRUE
now__::_thesis:_not_('not'_a)_._z_<>_TRUE
assume  ('not' a) . z <> TRUE ; ::_thesis: contradiction
then (('not' b) . z) '&' (('not' a) . z) = FALSE '&' (('not' b) . z) by XBOOLEAN:def_3
.= FALSE ;
hence  contradiction by A2, A1; ::_thesis: verum
end;
hence  ('not' a) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:4
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'or' b) '&' ('not' a) '<' b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'or' b) '&' ('not' a) '<' b
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) '&' ('not' a) '<' b
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'or' b) '&' ('not' a)) . z = TRUE or b . z = TRUE )
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 ; ::_thesis: b . z = TRUE
now__::_thesis:_not_b_._z_<>_TRUE
assume  b . z <> TRUE ; ::_thesis: contradiction
then (('not' a) . z) '&' (b . z) = FALSE '&' (('not' a) . z) by XBOOLEAN:def_3
.= FALSE ;
hence  contradiction by A2, A1; ::_thesis: verum
end;
hence  b . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:5
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' b) '<' b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' b) '<' b
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (('not' a) 'imp' b) '<' b
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (('not' a) 'imp' b)) . z = TRUE or b . z = TRUE )
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 ; ::_thesis: b . z = TRUE
now__::_thesis:_not_b_._z_<>_TRUE
assume  b . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  b . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:6
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' ('not' b)) '<' 'not' a
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' ('not' b)) '<' 'not' a
let a, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (a 'imp' ('not' b)) '<' 'not' a
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (a 'imp' ('not' b))) . z = TRUE or ('not' a) . z = TRUE )
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 ; ::_thesis: ('not' a) . z = TRUE
now__::_thesis:_not_('not'_a)_._z_<>_TRUE
assume  ('not' a) . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  ('not' a) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:7
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b '&' c) '<' a 'imp' b
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' (b '&' c) '<' a 'imp' b
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' (b '&' c) '<' a 'imp' b
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'imp' (b '&' c)) . z = TRUE or (a 'imp' b) . z = TRUE )
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 ; ::_thesis: (a 'imp' b) . z = TRUE
now__::_thesis:_not_(a_'imp'_b)_._z_<>_TRUE
assume  (a 'imp' b) . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  (a 'imp' b) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:8
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'imp' c '<' a 'imp' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) 'imp' c '<' a 'imp' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) 'imp' c '<' a 'imp' c
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'or' b) 'imp' c) . z = TRUE or (a 'imp' c) . z = TRUE )
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 ; ::_thesis: (a 'imp' c) . z = TRUE
now__::_thesis:_not_(a_'imp'_c)_._z_<>_TRUE
assume  (a 'imp' c) . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  (a 'imp' c) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:9
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a '&' c) 'imp' b
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a '&' c) 'imp' b
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' b '<' (a '&' c) 'imp' b
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'imp' b) . z = TRUE or ((a '&' c) 'imp' b) . z = TRUE )
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 ; ::_thesis: ((a '&' c) 'imp' b) . z = TRUE
now__::_thesis:_not_((a_'&'_c)_'imp'_b)_._z_<>_TRUE
assume  ((a '&' c) 'imp' b) . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  ((a '&' c) 'imp' b) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:10
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a '&' c) 'imp' (b '&' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a '&' c) 'imp' (b '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' b '<' (a '&' c) 'imp' (b '&' c)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'imp' b) . z = TRUE or ((a '&' c) 'imp' (b '&' c)) . z = TRUE )
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 ; ::_thesis: ((a '&' c) 'imp' (b '&' c)) . z = TRUE
now__::_thesis:_not_((a_'&'_c)_'imp'_(b_'&'_c))_._z_<>_TRUE
assume  ((a '&' c) 'imp' (b '&' c)) . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  ((a '&' c) 'imp' (b '&' c)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:11
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' a 'imp' (b 'or' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' a 'imp' (b 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' b '<' a 'imp' (b 'or' c)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'imp' b) . z = TRUE or (a 'imp' (b 'or' c)) . z = TRUE )
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 ; ::_thesis: (a 'imp' (b 'or' c)) . z = TRUE
now__::_thesis:_not_(a_'imp'_(b_'or'_c))_._z_<>_TRUE
assume A3: (a 'imp' (b 'or' c)) . z <> TRUE ; ::_thesis: contradiction
(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; ::_thesis: verum
end;
hence  (a 'imp' (b 'or' c)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:12
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a 'or' c) 'imp' (b 'or' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds a 'imp' b '<' (a 'or' c) 'imp' (b 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: a 'imp' b '<' (a 'or' c) 'imp' (b 'or' c)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (a 'imp' b) . z = TRUE or ((a 'or' c) 'imp' (b 'or' c)) . z = TRUE )
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 ; ::_thesis: ((a 'or' c) 'imp' (b 'or' c)) . z = TRUE
now__::_thesis:_not_((a_'or'_c)_'imp'_(b_'or'_c))_._z_<>_TRUE
assume A3: ((a 'or' c) 'imp' (b 'or' c)) . z <> TRUE ; ::_thesis: contradiction
((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; ::_thesis: verum
end;
hence  ((a 'or' c) 'imp' (b 'or' c)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:13
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'or' c '<' a 'or' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a '&' b) 'or' c '<' a 'or' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'or' c '<' a 'or' c
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a '&' b) 'or' c) . z = TRUE or (a 'or' c) . z = TRUE )
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 ; ::_thesis: (a 'or' c) . z = TRUE
now__::_thesis:_not_(a_'or'_c)_._z_<>_TRUE
assume  (a 'or' c) . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  (a 'or' c) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:14
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a '&' b) 'or' (c '&' d) '<' a 'or' c
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds (a '&' b) 'or' (c '&' d) '<' a 'or' c
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: (a '&' b) 'or' (c '&' d) '<' a 'or' c
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a '&' b) 'or' (c '&' d)) . z = TRUE or (a 'or' c) . z = TRUE )
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 ; ::_thesis: (a 'or' c) . z = TRUE
now__::_thesis:_not_(a_'or'_c)_._z_<>_TRUE
assume  (a 'or' c) . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  (a 'or' c) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:15
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (b 'imp' c) '<' a 'or' c by Th1;

theorem :: BVFUNC_9:16
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' c) '<' b 'or' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (('not' a) 'imp' c) '<' b 'or' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (('not' a) 'imp' c) '<' b 'or' c
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (('not' a) 'imp' c)) . z = TRUE or (b 'or' c) . z = TRUE )
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 ; ::_thesis: (b 'or' c) . z = TRUE
now__::_thesis:_not_(b_'or'_c)_._z_<>_TRUE
reconsider az = a . z as boolean set ;
assume  (b 'or' c) . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  (b 'or' c) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:17
for Y being non empty set
for a, c, b being Function of Y,BOOLEAN holds (a 'imp' c) '&' (b 'imp' ('not' c)) '<' ('not' a) 'or' ('not' b)
proof
let Y be non empty set ; ::_thesis: for a, c, b being Function of Y,BOOLEAN holds (a 'imp' c) '&' (b 'imp' ('not' c)) '<' ('not' a) 'or' ('not' b)
let a, c, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' c) '&' (b 'imp' ('not' c)) '<' ('not' a) 'or' ('not' b)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' c) '&' (b 'imp' ('not' c))) . z = TRUE or (('not' a) 'or' ('not' b)) . z = TRUE )
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 ; ::_thesis: (('not' a) 'or' ('not' b)) . z = TRUE
now__::_thesis:_not_(('not'_a)_'or'_('not'_b))_._z_<>_TRUE
assume  (('not' a) 'or' ('not' b)) . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  (('not' a) 'or' ('not' b)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:18
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' c) '<' b 'or' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'or' b) '&' (('not' a) 'or' c) '<' b 'or' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) '&' (('not' a) 'or' c) '<' b 'or' c
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'or' b) '&' (('not' a) 'or' c)) . z = TRUE or (b 'or' c) . z = TRUE )
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 ; ::_thesis: (b 'or' c) . z = TRUE
now__::_thesis:_not_(b_'or'_c)_._z_<>_TRUE
assume  (b 'or' c) . z <> TRUE ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  (b 'or' c) . z = TRUE ; ::_thesis: verum
end;

theorem Th19: :: BVFUNC_9:19
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' b) '&' (c 'imp' d) '<' (a '&' c) 'imp' (b '&' d)
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' b) '&' (c 'imp' d) '<' (a '&' c) 'imp' (b '&' d)
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (c 'imp' d) '<' (a '&' c) 'imp' (b '&' d)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (c 'imp' d)) . z = TRUE or ((a '&' c) 'imp' (b '&' d)) . z = TRUE )
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 ; ::_thesis: ((a '&' c) 'imp' (b '&' d)) . z = TRUE
now__::_thesis:_(_((a_'&'_c)_'imp'_(b_'&'_d))_._z_<>_TRUE_implies_((a_'&'_c)_'imp'_(b_'&'_d))_._z_=_TRUE_)
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 ; ::_thesis: ((a '&' c) 'imp' (b '&' d)) . z = TRUE
now__::_thesis:_(_(_b_._z_=_FALSE_&_((a_'&'_c)_'imp'_(b_'&'_d))_._z_=_TRUE_)_or_(_d_._z_=_FALSE_&_((a_'&'_c)_'imp'_(b_'&'_d))_._z_=_TRUE_)_)
percases ( b . z = FALSE or d . z = FALSE ) by A7, A6, A5, MARGREL1:12;
case b . z = FALSE ; ::_thesis: ((a '&' c) 'imp' (b '&' d)) . z = TRUE
thus  ((a '&' c) 'imp' (b '&' d)) . z = TRUE by A2, A1, A6, A4, A3; ::_thesis: verum
end;
case d . z = FALSE ; ::_thesis: ((a '&' c) 'imp' (b '&' d)) . z = TRUE
thus  ((a '&' c) 'imp' (b '&' d)) . z = TRUE by A2, A1, A6, A4, A3; ::_thesis: verum
end;
end;
end;
hence  ((a '&' c) 'imp' (b '&' d)) . z = TRUE ; ::_thesis: verum
end;
hence  ((a '&' c) 'imp' (b '&' d)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:20
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b '&' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b '&' c)
 (a 'imp' b) '&' (a 'imp' c) '<' (a '&' a) 'imp' (b '&' c) by Th19;
hence  (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b '&' c) ; ::_thesis: verum
end;

theorem Th21: :: BVFUNC_9:21
for Y being non empty set
for a, c, b being Function of Y,BOOLEAN holds (a 'imp' c) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c
proof
let Y be non empty set ; ::_thesis: for a, c, b being Function of Y,BOOLEAN holds (a 'imp' c) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c
let a, c, b be Function of Y,BOOLEAN; ::_thesis: (a 'imp' c) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c
 ((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c) = I_el Y by BVFUNC_6:9;
hence  (a 'imp' c) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c by BVFUNC_1:16; ::_thesis: verum
end;

theorem Th22: :: BVFUNC_9:22
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' b) '&' (c 'imp' d) '<' (a 'or' c) 'imp' (b 'or' d)
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds (a 'imp' b) '&' (c 'imp' d) '<' (a 'or' c) 'imp' (b 'or' d)
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (c 'imp' d) '<' (a 'or' c) 'imp' (b 'or' d)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (c 'imp' d)) . z = TRUE or ((a 'or' c) 'imp' (b 'or' d)) . z = TRUE )
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 ; ::_thesis: ((a 'or' c) 'imp' (b 'or' d)) . z = TRUE
now__::_thesis:_(_((a_'or'_c)_'imp'_(b_'or'_d))_._z_<>_TRUE_implies_((a_'or'_c)_'imp'_(b_'or'_d))_._z_=_TRUE_)
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 ; ::_thesis: ((a 'or' c) 'imp' (b 'or' d)) . z = TRUE
now__::_thesis:_(_(_('not'_a)_._z_=_FALSE_&_((a_'or'_c)_'imp'_(b_'or'_d))_._z_=_TRUE_)_or_(_('not'_c)_._z_=_FALSE_&_((a_'or'_c)_'imp'_(b_'or'_d))_._z_=_TRUE_)_)
percases ( ('not' a) . z = FALSE or ('not' c) . z = FALSE ) by A7, A6, A5, MARGREL1:12;
case ('not' a) . z = FALSE ; ::_thesis: ((a 'or' c) 'imp' (b 'or' d)) . z = TRUE
thus  ((a 'or' c) 'imp' (b 'or' d)) . z = TRUE by A2, A1, A6, A4, A3; ::_thesis: verum
end;
case ('not' c) . z = FALSE ; ::_thesis: ((a 'or' c) 'imp' (b 'or' d)) . z = TRUE
thus  ((a 'or' c) 'imp' (b 'or' d)) . z = TRUE by A2, A1, A6, A4, A3; ::_thesis: verum
end;
end;
end;
hence  ((a 'or' c) 'imp' (b 'or' d)) . z = TRUE ; ::_thesis: verum
end;
hence  ((a 'or' c) 'imp' (b 'or' d)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC_9:23
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b 'or' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b 'or' c)
 (a 'imp' b) '&' (a 'imp' c) '<' (a 'or' a) 'imp' (b 'or' c) by Th22;
hence  (a 'imp' b) '&' (a 'imp' c) '<' a 'imp' (b 'or' c) ; ::_thesis: verum
end;

theorem Th24: :: BVFUNC_9:24
for Y being non empty set
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 Y be non empty set ; ::_thesis: 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
let a1, b1, c1, a2, b2, c2 be Function of Y,BOOLEAN; ::_thesis: ((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' a2 'imp' a1
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  ((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' a2 'imp' a1 by BVFUNC_1:16; ::_thesis: verum
end;

Lm8:  for Y being non empty set
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 Y be non empty set ; ::_thesis: 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
let a1, b1, c1, a2, b2, c2 be Function of Y,BOOLEAN; ::_thesis: (((((((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: (((((((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  (((((((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 A3, BVFUNC_6:18; ::_thesis: verum
end;

Lm9:  for Y being non empty set
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 Y be non empty set ; ::_thesis: 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
let a1, b1, c1, a2, b2, c2 be Function of Y,BOOLEAN; ::_thesis: (((((((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
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  (((((((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 A3, BVFUNC_6:18; ::_thesis: verum
end;

Lm10:  for Y being non empty set
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 Y be non empty set ; ::_thesis: 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
let a1, b1, c1, a2, b2, c2 be Function of Y,BOOLEAN; ::_thesis: (((((((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
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  (((((((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 A3, BVFUNC_6:18; ::_thesis: verum
end;

theorem :: BVFUNC_9:25
for Y being non empty set
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 Y be non empty set ; ::_thesis: 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)
let a1, b1, c1, a2, b2, c2 be Function of Y,BOOLEAN; ::_thesis: ((((((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)
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  ((((((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) by BVFUNC_1:16; ::_thesis: verum
end;

theorem Th26: :: BVFUNC_9:26
for Y being non empty set
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 Y be non empty set ; ::_thesis: 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
let a1, b1, a2, b2 be Function of Y,BOOLEAN; ::_thesis: (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) 'imp' ('not' (a1 '&' b1)) = I_el Y
 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; ::_thesis: ( (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) . z = TRUE implies ('not' (a1 '&' b1)) . z = TRUE )
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 ; ::_thesis: ('not' (a1 '&' b1)) . z = TRUE
now__::_thesis:_not_('not'_(a1_'&'_b1))_._z_<>_TRUE
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 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  ('not' (a1 '&' b1)) . z = TRUE ; ::_thesis: verum
end;
hence  (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) 'imp' ('not' (a1 '&' b1)) = I_el Y by BVFUNC_1:16, BVFUNC_1:def_12; ::_thesis: verum
end;

theorem :: BVFUNC_9:27
for Y being non empty set
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 Y be non empty set ; ::_thesis: 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))
let a1, b1, c1, a2, b2, c2 be Function of Y,BOOLEAN; ::_thesis: (((((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))
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  (((((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)) by A6, BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC_9:28
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b '<' a by Lm1;

theorem :: BVFUNC_9:29
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds
( (a '&' b) '&' c '<' a & (a '&' b) '&' c '<' b ) by Lm2;

theorem :: BVFUNC_9:30
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds
( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b ) by Lm3;

theorem :: BVFUNC_9:31
for Y being non empty set
for a, b, c, d, e being Function of Y,BOOLEAN holds
( (((a '&' b) '&' c) '&' d) '&' e '<' a & (((a '&' b) '&' c) '&' d) '&' e '<' b ) by Lm4;

theorem :: BVFUNC_9:32
for Y being non empty set
for a, b, c, d, e, f being Function of Y,BOOLEAN holds
( ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' a & ((((a '&' b) '&' c) '&' d) '&' e) '&' f '<' b ) by Lm5;

theorem :: BVFUNC_9:33
for Y being non empty set
for a, b, c, d, e, f, g being Function of Y,BOOLEAN holds
( (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' a & (((((a '&' b) '&' c) '&' d) '&' e) '&' f) '&' g '<' b ) by Lm6;

theorem Th34: :: BVFUNC_9:34
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a '<' b & c '<' d holds
a '&' c '<' b '&' d
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a '<' b & c '<' d holds
a '&' c '<' b '&' d
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a '<' b & c '<' d implies a '&' c '<' b '&' d )
assume  ( a '<' b & c '<' d ) ; ::_thesis: a '&' c '<' b '&' 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  a '&' c '<' b '&' d by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC_9:35
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds
a '&' ('not' c) '<' 'not' b
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds
a '&' ('not' c) '<' 'not' b
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a '&' b '<' c implies a '&' ('not' c) '<' 'not' b )
assume  a '&' b '<' c ; ::_thesis: a '&' ('not' c) '<' 'not' b
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  a '&' ('not' c) '<' 'not' b by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC_9:36
for Y being non empty set
for a, c, b being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' c
proof
let Y be non empty set ; ::_thesis: for a, c, b being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' c
let a, c, b be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' c
set K1 = (a 'imp' c) '&' (b 'imp' c);
 (a 'imp' c) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c by Th21;
then A1: ((a 'imp' c) '&' (b 'imp' c)) '&' (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  ((a 'imp' c) '&' (b 'imp' c)) '&' (a 'or' b) '<' c by A1, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC_9:37
for Y being non empty set
for a, c, b being Function of Y,BOOLEAN holds ((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c
proof
let Y be non empty set ; ::_thesis: for a, c, b being Function of Y,BOOLEAN holds ((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c
let a, c, b be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c
 (a 'imp' c) 'or' (b 'imp' c) = (a '&' b) 'imp' c by BVFUNC_7:6;
hence  ((a 'imp' c) 'or' (b 'imp' c)) '&' (a '&' b) '<' c by Th2; ::_thesis: verum
end;

theorem :: BVFUNC_9:38
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a '<' b & c '<' d holds
a 'or' c '<' b 'or' d
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN st a '<' b & c '<' d holds
a 'or' c '<' b 'or' d
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ( a '<' b & c '<' d implies a 'or' c '<' b 'or' d )
assume  ( a '<' b & c '<' d ) ; ::_thesis: a 'or' c '<' b 'or' 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  a 'or' c '<' b 'or' d by BVFUNC_1:16; ::_thesis: verum
end;

theorem Th39: :: BVFUNC_9:39
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '<' a 'or' b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '<' a 'or' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a '<' a 'or' b
 a 'imp' (a 'or' b) = I_el Y by BVFUNC_6:26;
hence  a '<' a 'or' b by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC_9:40
for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b '<' a 'or' b
proof
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN holds a '&' b '<' a 'or' b
let a, b be Function of Y,BOOLEAN; ::_thesis: a '&' b '<' a 'or' b
 ( a '&' b '<' a & a '<' a 'or' b ) by Lm1, Th39;
hence  a '&' b '<' a 'or' b by BVFUNC_1:15; ::_thesis: verum
end;