:: BVFUNC10 semantic presentation

begin

theorem :: BVFUNC10:1
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) = ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) = ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) = ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)
 for z being Element of Y st (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE holds
(((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE
proof
let z be Element of Y; ::_thesis: ( (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE implies (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE )
A1: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = (((a '&' b) 'or' (b '&' c)) . z) 'or' ((c '&' a) . z) by BVFUNC_1:def_4
.= (((a '&' b) . z) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by BVFUNC_1:def_4
.= (((a . z) '&' (b . z)) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c '&' a) . z) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c . z) '&' (a . z)) by MARGREL1:def_20 ;
assume A2: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE
now__::_thesis:_(_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_<>_TRUE_implies_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_=_TRUE_)
A3: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = (((a 'or' b) '&' (b 'or' c)) . z) '&' ((c 'or' a) . z) by MARGREL1:def_20
.= (((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by MARGREL1:def_20
.= (((a . z) 'or' (b . z)) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by BVFUNC_1:def_4
.= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c 'or' a) . z) by BVFUNC_1:def_4
.= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z)) by BVFUNC_1:def_4 ;
assume Z: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z <> TRUE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE
now__::_thesis:_(_(_((a_._z)_'or'_(b_._z))_'&'_((b_._z)_'or'_(c_._z))_=_FALSE_&_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_=_TRUE_)_or_(_(c_._z)_'or'_(a_._z)_=_FALSE_&_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_=_TRUE_)_)
percases ( ((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z)) = FALSE or (c . z) 'or' (a . z) = FALSE ) by Z, MARGREL1:12, A3, XBOOLEAN:def_3;
caseA5: ((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z)) = FALSE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE
now__::_thesis:_(_(_(a_._z)_'or'_(b_._z)_=_FALSE_&_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_=_TRUE_)_or_(_(b_._z)_'or'_(c_._z)_=_FALSE_&_(((a_'or'_b)_'&'_(b_'or'_c))_'&'_(c_'or'_a))_._z_=_TRUE_)_)
percases ( (a . z) 'or' (b . z) = FALSE or (b . z) 'or' (c . z) = FALSE ) by A5, MARGREL1:12;
caseA6: (a . z) 'or' (b . z) = FALSE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE
 ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3;
hence  (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE by A2, A1, A6; ::_thesis: verum
end;
caseA7: (b . z) 'or' (c . z) = FALSE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE
 ( c . z = TRUE or c . z = FALSE ) by XBOOLEAN:def_3;
hence  (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE by A2, A1, A7; ::_thesis: verum
end;
end;
end;
hence  (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ; ::_thesis: verum
end;
caseA8: (c . z) 'or' (a . z) = FALSE ; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE
 ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3;
hence  (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE by A2, A1, A8; ::_thesis: verum
end;
end;
end;
hence  (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ; ::_thesis: verum
end;
hence  (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ; ::_thesis: verum
end;
then A9: ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) '<' ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a) by BVFUNC_1:def_12;
 for z being Element of Y st (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE holds
(((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE
proof
let z be Element of Y; ::_thesis: ( (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE implies (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE )
A10: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = (((a 'or' b) '&' (b 'or' c)) . z) '&' ((c 'or' a) . z) by MARGREL1:def_20
.= (((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by MARGREL1:def_20
.= (((a . z) 'or' (b . z)) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z) by BVFUNC_1:def_4
.= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c 'or' a) . z) by BVFUNC_1:def_4
.= (((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z)) by BVFUNC_1:def_4 ;
assume A11: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z = TRUE ; ::_thesis: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE
now__::_thesis:_(_(((a_'&'_b)_'or'_(b_'&'_c))_'or'_(c_'&'_a))_._z_<>_TRUE_implies_(((a_'&'_b)_'or'_(b_'&'_c))_'or'_(c_'&'_a))_._z_=_TRUE_)
A12: ( (b . z) '&' (c . z) = TRUE or (b . z) '&' (c . z) = FALSE ) by XBOOLEAN:def_3;
A13: ( (c . z) '&' (a . z) = TRUE or (c . z) '&' (a . z) = FALSE ) by XBOOLEAN:def_3;
A15: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = (((a '&' b) 'or' (b '&' c)) . z) 'or' ((c '&' a) . z) by BVFUNC_1:def_4
.= (((a '&' b) . z) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by BVFUNC_1:def_4
.= (((a . z) '&' (b . z)) 'or' ((b '&' c) . z)) 'or' ((c '&' a) . z) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c '&' a) . z) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) 'or' ((b . z) '&' (c . z))) 'or' ((c . z) '&' (a . z)) by MARGREL1:def_20 ;
assume A16: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z <> TRUE ; ::_thesis: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE
now__::_thesis:_(_(_a_._z_=_FALSE_&_b_._z_=_FALSE_&_(((a_'&'_b)_'or'_(b_'&'_c))_'or'_(c_'&'_a))_._z_=_TRUE_)_or_(_b_._z_=_FALSE_&_c_._z_=_FALSE_&_(((a_'&'_b)_'or'_(b_'&'_c))_'or'_(c_'&'_a))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_a_._z_=_FALSE_&_(((a_'&'_b)_'or'_(b_'&'_c))_'or'_(c_'&'_a))_._z_=_TRUE_)_)
percases ( ( a . z = FALSE & b . z = FALSE ) or ( b . z = FALSE & c . z = FALSE ) or ( c . z = FALSE & a . z = FALSE ) ) by A16, A15, XBOOLEAN:def_3, A13, A12, MARGREL1:12;
case ( a . z = FALSE & b . z = FALSE ) ; ::_thesis: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE
hence  (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE by A11, A10; ::_thesis: verum
end;
case ( b . z = FALSE & c . z = FALSE ) ; ::_thesis: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE
hence  (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE by A11, A10; ::_thesis: verum
end;
case ( c . z = FALSE & a . z = FALSE ) ; ::_thesis: (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE
hence  (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE by A11, A10; ::_thesis: verum
end;
end;
end;
hence  (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE ; ::_thesis: verum
end;
hence  (((a '&' b) 'or' (b '&' c)) 'or' (c '&' a)) . z = TRUE ; ::_thesis: verum
end;
then  ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a) '<' ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) by BVFUNC_1:def_12;
hence  ((a '&' b) 'or' (b '&' c)) 'or' (c '&' a) = ((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a) by A9, BVFUNC_1:15; ::_thesis: verum
end;

Lm1:  for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) '<' ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) '<' ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a)) '<' ((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a))) . z = TRUE or (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE )
A1: (((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a))) . z = (((a '&' ('not' b)) 'or' (b '&' ('not' c))) . z) 'or' ((c '&' ('not' a)) . z) by BVFUNC_1:def_4
.= (((a '&' ('not' b)) . z) 'or' ((b '&' ('not' c)) . z)) 'or' ((c '&' ('not' a)) . z) by BVFUNC_1:def_4
.= (((a . z) '&' (('not' b) . z)) 'or' ((b '&' ('not' c)) . z)) 'or' ((c '&' ('not' a)) . z) by MARGREL1:def_20
.= (((a . z) '&' (('not' b) . z)) 'or' ((b . z) '&' (('not' c) . z))) 'or' ((c '&' ('not' a)) . z) by MARGREL1:def_20
.= (((a . z) '&' (('not' b) . z)) 'or' ((b . z) '&' (('not' c) . z))) 'or' ((c . z) '&' (('not' a) . z)) by MARGREL1:def_20
.= (((a . z) '&' ('not' (b . z))) 'or' ((b . z) '&' (('not' c) . z))) 'or' ((c . z) '&' (('not' a) . z)) by MARGREL1:def_19
.= (((a . z) '&' ('not' (b . z))) 'or' ((b . z) '&' ('not' (c . z)))) 'or' ((c . z) '&' (('not' a) . z)) by MARGREL1:def_19
.= (((a . z) '&' ('not' (b . z))) 'or' ((b . z) '&' ('not' (c . z)))) 'or' ((c . z) '&' ('not' (a . z))) by MARGREL1:def_19 ;
assume A2: (((a '&' ('not' b)) 'or' (b '&' ('not' c))) 'or' (c '&' ('not' a))) . z = TRUE ; ::_thesis: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE
now__::_thesis:_(_(((b_'&'_('not'_a))_'or'_(c_'&'_('not'_b)))_'or'_(a_'&'_('not'_c)))_._z_<>_TRUE_implies_(((b_'&'_('not'_a))_'or'_(c_'&'_('not'_b)))_'or'_(a_'&'_('not'_c)))_._z_=_TRUE_)
A3: ( (a . z) '&' (('not' c) . z) = TRUE or (a . z) '&' (('not' c) . z) = FALSE ) by XBOOLEAN:def_3;
assume A4: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z <> TRUE ; ::_thesis: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE
A5: ( (c . z) '&' (('not' b) . z) = TRUE or (c . z) '&' (('not' b) . z) = FALSE ) by XBOOLEAN:def_3;
A6: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = (((b '&' ('not' a)) 'or' (c '&' ('not' b))) . z) 'or' ((a '&' ('not' c)) . z) by BVFUNC_1:def_4
.= (((b '&' ('not' a)) . z) 'or' ((c '&' ('not' b)) . z)) 'or' ((a '&' ('not' c)) . z) by BVFUNC_1:def_4
.= (((b . z) '&' (('not' a) . z)) 'or' ((c '&' ('not' b)) . z)) 'or' ((a '&' ('not' c)) . z) by MARGREL1:def_20
.= (((b . z) '&' (('not' a) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' ((a '&' ('not' c)) . z) by MARGREL1:def_20
.= (((b . z) '&' (('not' a) . z)) 'or' ((c . z) '&' (('not' b) . z))) 'or' ((a . z) '&' (('not' c) . z)) by MARGREL1:def_20 ;
 ( ((b . z) '&' (('not' a) . z)) 'or' ((c . z) '&' (('not' b) . z)) = TRUE or ((b . z) '&' (('not' a) . z)) 'or' ((c . z) '&' (('not' b) . z)) = FALSE ) by XBOOLEAN:def_3;
then A7: ( b . z = FALSE or ('not' a) . z = FALSE ) by A4, A6, A5, MARGREL1:12;
now__::_thesis:_(_(_a_._z_=_FALSE_&_(((b_'&'_('not'_a))_'or'_(c_'&'_('not'_b)))_'or'_(a_'&'_('not'_c)))_._z_=_TRUE_)_or_(_('not'_c)_._z_=_FALSE_&_(((b_'&'_('not'_a))_'or'_(c_'&'_('not'_b)))_'or'_(a_'&'_('not'_c)))_._z_=_TRUE_)_)
percases ( a . z = FALSE or ('not' c) . z = FALSE ) by A4, A6, A3, MARGREL1:12;
case a . z = FALSE ; ::_thesis: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE
hence  (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE by A2, A1, A6, A7, MARGREL1:def_19; ::_thesis: verum
end;
case ('not' c) . z = FALSE ; ::_thesis: (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE
then A8: 'not' (c . z) = FALSE by MARGREL1:def_19;
then  'not' (b . z) = FALSE by A4, A6, A5, MARGREL1:def_19;
hence  (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE by A2, A1, A6, A5, A8, MARGREL1:def_19; ::_thesis: verum
end;
end;
end;
hence  (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
hence  (((b '&' ('not' a)) 'or' (c '&' ('not' b))) 'or' (a '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;

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

Lm2:  for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a))) . z = TRUE or (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE )
A1: (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a))) . z = (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) . z) '&' ((c 'or' ('not' a)) . z) by MARGREL1:def_20
.= (((a 'or' ('not' b)) . z) '&' ((b 'or' ('not' c)) . z)) '&' ((c 'or' ('not' a)) . z) by MARGREL1:def_20
.= (((a . z) 'or' (('not' b) . z)) '&' ((b 'or' ('not' c)) . z)) '&' ((c 'or' ('not' a)) . z) by BVFUNC_1:def_4
.= (((a . z) 'or' (('not' b) . z)) '&' ((b . z) 'or' (('not' c) . z))) '&' ((c 'or' ('not' a)) . z) by BVFUNC_1:def_4
.= (((a . z) 'or' (('not' b) . z)) '&' ((b . z) 'or' (('not' c) . z))) '&' ((c . z) 'or' (('not' a) . z)) by BVFUNC_1:def_4
.= (((a . z) 'or' ('not' (b . z))) '&' ((b . z) 'or' (('not' c) . z))) '&' ((c . z) 'or' (('not' a) . z)) by MARGREL1:def_19
.= (((a . z) 'or' ('not' (b . z))) '&' ((b . z) 'or' ('not' (c . z)))) '&' ((c . z) 'or' (('not' a) . z)) by MARGREL1:def_19
.= (((a . z) 'or' ('not' (b . z))) '&' ((b . z) 'or' ('not' (c . z)))) '&' ((c . z) 'or' ('not' (a . z))) by MARGREL1:def_19 ;
assume A2: (((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a))) . z = TRUE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE
now__::_thesis:_(_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_<>_TRUE_implies_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_=_TRUE_)
A3: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) . z) '&' ((a 'or' ('not' c)) . z) by MARGREL1:def_20
.= (((b 'or' ('not' a)) . z) '&' ((c 'or' ('not' b)) . z)) '&' ((a 'or' ('not' c)) . z) by MARGREL1:def_20
.= (((b . z) 'or' (('not' a) . z)) '&' ((c 'or' ('not' b)) . z)) '&' ((a 'or' ('not' c)) . z) by BVFUNC_1:def_4
.= (((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z))) '&' ((a 'or' ('not' c)) . z) by BVFUNC_1:def_4
.= (((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z))) '&' ((a . z) 'or' (('not' c) . z)) by BVFUNC_1:def_4 ;
assume Z: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z <> TRUE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE
now__::_thesis:_(_(_((b_._z)_'or'_(('not'_a)_._z))_'&'_((c_._z)_'or'_(('not'_b)_._z))_=_FALSE_&_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_=_TRUE_)_or_(_(a_._z)_'or'_(('not'_c)_._z)_=_FALSE_&_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_=_TRUE_)_)
percases ( ((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z)) = FALSE or (a . z) 'or' (('not' c) . z) = FALSE ) by Z, A3, XBOOLEAN:def_3, MARGREL1:12;
caseA5: ((b . z) 'or' (('not' a) . z)) '&' ((c . z) 'or' (('not' b) . z)) = FALSE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE
now__::_thesis:_(_(_(b_._z)_'or'_(('not'_a)_._z)_=_FALSE_&_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_=_TRUE_)_or_(_(c_._z)_'or'_(('not'_b)_._z)_=_FALSE_&_(((b_'or'_('not'_a))_'&'_(c_'or'_('not'_b)))_'&'_(a_'or'_('not'_c)))_._z_=_TRUE_)_)
percases ( (b . z) 'or' (('not' a) . z) = FALSE or (c . z) 'or' (('not' b) . z) = FALSE ) by A5, MARGREL1:12;
caseA6: (b . z) 'or' (('not' a) . z) = FALSE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE
A7: ( ('not' a) . z = TRUE or ('not' a) . z = FALSE ) by XBOOLEAN:def_3;
then  'not' (a . z) = FALSE by A6, MARGREL1:def_19;
hence  (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE by A2, A1, A6, A7, XBOOLEAN:138; ::_thesis: verum
end;
caseA8: (c . z) 'or' (('not' b) . z) = FALSE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE
A9: ( ('not' b) . z = TRUE or ('not' b) . z = FALSE ) by XBOOLEAN:def_3;
then  'not' (b . z) = FALSE by A8, MARGREL1:def_19;
hence  (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE by A2, A1, A8, A9, XBOOLEAN:138; ::_thesis: verum
end;
end;
end;
hence  (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
caseA10: (a . z) 'or' (('not' c) . z) = FALSE ; ::_thesis: (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE
A11: ( ('not' c) . z = TRUE or ('not' c) . z = FALSE ) by XBOOLEAN:def_3;
then  'not' (c . z) = FALSE by A10, MARGREL1:def_19;
hence  (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE by A2, A1, A10, A11, XBOOLEAN:138; ::_thesis: verum
end;
end;
end;
hence  (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
hence  (((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC10:3
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c))
 ( ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) '<' ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) & ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) '<' ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) ) by Lm2;
hence  ((a 'or' ('not' b)) '&' (b 'or' ('not' c))) '&' (c 'or' ('not' a)) = ((b 'or' ('not' a)) '&' (c 'or' ('not' b))) '&' (a 'or' ('not' c)) by BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC10:4
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st c 'imp' a = I_el Y & c 'imp' b = I_el Y holds
c 'imp' (a 'or' b) = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st c 'imp' a = I_el Y & c 'imp' b = I_el Y holds
c 'imp' (a 'or' b) = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( c 'imp' a = I_el Y & c 'imp' b = I_el Y implies c 'imp' (a 'or' b) = I_el Y )
assume A1: ( c 'imp' a = I_el Y & c 'imp' b = I_el Y ) ; ::_thesis: c 'imp' (a 'or' b) = I_el Y
c 'imp' (a 'or' b) = (c 'imp' a) 'or' (c 'imp' b) by BVFUNC_7:3
.= I_el Y by A1 ;
hence  c 'imp' (a 'or' b) = I_el Y ; ::_thesis: verum
end;

theorem :: BVFUNC10:5
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a 'imp' c = I_el Y & b 'imp' c = I_el Y holds
(a '&' b) 'imp' c = I_el Y
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN st a 'imp' c = I_el Y & b 'imp' c = I_el Y holds
(a '&' b) 'imp' c = I_el Y
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ( a 'imp' c = I_el Y & b 'imp' c = I_el Y implies (a '&' b) 'imp' c = I_el Y )
 ( a 'imp' c = I_el Y & b 'imp' c = I_el Y implies (a '&' b) 'imp' (c '&' c) = I_el Y ) by BVFUNC_6:21;
hence  ( a 'imp' c = I_el Y & b 'imp' c = I_el Y implies (a '&' b) 'imp' c = I_el Y ) ; ::_thesis: verum
end;

theorem :: BVFUNC10:6
for Y being non empty set
for a1, a2, b1, b2, c1, c2 being Function of Y,BOOLEAN holds (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1) '<' (a2 'or' b2) 'or' c2
proof
let Y be non empty set ; ::_thesis: for a1, a2, b1, b2, c1, c2 being Function of Y,BOOLEAN holds (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1) '<' (a2 'or' b2) 'or' c2
let a1, a2, b1, b2, c1, c2 be Function of Y,BOOLEAN; ::_thesis: (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1) '<' (a2 'or' b2) 'or' c2
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) . z = TRUE or ((a2 'or' b2) 'or' c2) . z = TRUE )
A1: ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) . z = ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) . z) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def_20
.= ((((a1 'imp' a2) '&' (b1 'imp' b2)) . z) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def_20
.= ((((a1 'imp' a2) . z) '&' ((b1 'imp' b2) . z)) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def_20
.= ((((('not' a1) 'or' a2) . z) '&' ((b1 'imp' b2) . z)) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_4:8
.= ((((('not' a1) 'or' a2) . z) '&' ((('not' b1) 'or' b2) . z)) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_4:8
.= ((((('not' a1) 'or' a2) . z) '&' ((('not' b1) 'or' b2) . z)) '&' ((('not' c1) 'or' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_4:8
.= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) 'or' b2) . z)) '&' ((('not' c1) 'or' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def_4
.= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) 'or' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def_4
.= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def_4
.= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 'or' b1) . z) 'or' (c1 . z)) by BVFUNC_1:def_4
.= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by BVFUNC_1:def_4
.= (((('not' (a1 . z)) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def_19
.= (((('not' (a1 . z)) 'or' (a2 . z)) '&' (('not' (b1 . z)) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def_19
.= (((('not' (a1 . z)) 'or' (a2 . z)) '&' (('not' (b1 . z)) 'or' (b2 . z))) '&' (('not' (c1 . z)) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def_19 ;
assume A2: ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) . z = TRUE ; ::_thesis: ((a2 'or' b2) 'or' c2) . z = TRUE
now__::_thesis:_not_((a2_'or'_b2)_'or'_c2)_._z_<>_TRUE
A3: ( b2 . z = TRUE or b2 . z = FALSE ) by XBOOLEAN:def_3;
A4: ( c2 . z = TRUE or c2 . z = FALSE ) by XBOOLEAN:def_3;
A5: ((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' ((a1 'or' b1) 'or' c1) = (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' c1) by BVFUNC_1:12
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' ((('not' a1) '&' ('not' b1)) '&' (('not' c1) '&' c1)) by BVFUNC_1:4
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' ((('not' a1) '&' ('not' b1)) '&' (O_el Y)) by BVFUNC_4:5
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' (O_el Y) by BVFUNC_1:5
.= ((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1) by BVFUNC_1:9
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' b1) by BVFUNC_1:12
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' (((('not' a1) '&' ('not' c1)) '&' ('not' b1)) '&' b1) by BVFUNC_1:4
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' ((('not' a1) '&' ('not' c1)) '&' (('not' b1) '&' b1)) by BVFUNC_1:4
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' ((('not' a1) '&' ('not' c1)) '&' (O_el Y)) by BVFUNC_4:5
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' (O_el Y) by BVFUNC_1:5
.= ((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1 by BVFUNC_1:9
.= ((('not' b1) '&' ('not' c1)) '&' ('not' a1)) '&' a1 by BVFUNC_1:4
.= (('not' b1) '&' ('not' c1)) '&' (('not' a1) '&' a1) by BVFUNC_1:4
.= (('not' b1) '&' ('not' c1)) '&' (O_el Y) by BVFUNC_4:5
.= O_el Y by BVFUNC_1:5 ;
A6: ( (a2 . z) 'or' (b2 . z) = TRUE or (a2 . z) 'or' (b2 . z) = FALSE ) by XBOOLEAN:def_3;
A7: ((a2 'or' b2) 'or' c2) . z = ((a2 'or' b2) . z) 'or' (c2 . z) by BVFUNC_1:def_4
.= ((a2 . z) 'or' (b2 . z)) 'or' (c2 . z) by BVFUNC_1:def_4 ;
assume  ((a2 'or' b2) 'or' c2) . z <> TRUE ; ::_thesis: contradiction
then (((('not' (a1 . z)) 'or' (a2 . z)) '&' (('not' (b1 . z)) 'or' (b2 . z))) '&' (('not' (c1 . z)) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) = (((('not' a1) . z) '&' ('not' (b1 . z))) '&' ('not' (c1 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by A7, A6, A4, A3, MARGREL1:def_19
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' ('not' (c1 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def_19
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def_19
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 'or' b1) . z) 'or' (c1 . z)) by BVFUNC_1:def_4
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def_4
.= (((('not' a1) '&' ('not' b1)) . z) '&' (('not' c1) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def_20
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) . z) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def_20
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' ((a1 'or' b1) 'or' c1)) . z by MARGREL1:def_20 ;
hence  contradiction by A2, A1, A5, BVFUNC_1:def_10; ::_thesis: verum
end;
hence  ((a2 'or' b2) 'or' c2) . z = TRUE ; ::_thesis: verum
end;

Lm3:  for Y being non empty set
for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))
proof
let Y be non empty set ; ::_thesis: for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))
let a1, a2, b1, b2 be Function of Y,BOOLEAN; ::_thesis: (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z = TRUE or ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE )
A1: ((((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z = ((((('not' a1) 'or' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z by BVFUNC_4:8
.= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z by BVFUNC_4:8
.= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) '&' (a1 'or' a2)) . z) '&' (('not' (b1 '&' b2)) . z) by MARGREL1:def_20
.= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) . z) '&' ((a1 'or' a2) . z)) '&' (('not' (b1 '&' b2)) . z) by MARGREL1:def_20
.= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) . z) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:14
.= ((((('not' a1) 'or' b1) . z) '&' ((('not' a2) 'or' b2) . z)) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by MARGREL1:def_20
.= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) 'or' b2) . z)) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:def_4
.= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:def_4
.= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:def_4
.= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) . z) 'or' (('not' b2) . z)) by BVFUNC_1:def_4
.= (((('not' (a1 . z)) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) . z) 'or' (('not' b2) . z)) by MARGREL1:def_19
.= (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) . z) 'or' (('not' b2) . z)) by MARGREL1:def_19
.= (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' (('not' b2) . z)) by MARGREL1:def_19
.= (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) by MARGREL1:def_19 ;
assume A2: ((((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z = TRUE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE
now__::_thesis:_(_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_<>_TRUE_implies_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)
A3: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = ((((('not' b1) 'or' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z by BVFUNC_4:8
.= ((((('not' b1) 'or' a1) '&' (('not' b2) 'or' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z by BVFUNC_4:8
.= ((((('not' b1) 'or' a1) '&' (('not' b2) 'or' a2)) '&' (b1 'or' b2)) . z) '&' (('not' (a1 '&' a2)) . z) by MARGREL1:def_20
.= ((((('not' b1) 'or' a1) '&' (('not' b2) 'or' a2)) . z) '&' ((b1 'or' b2) . z)) '&' (('not' (a1 '&' a2)) . z) by MARGREL1:def_20
.= ((((('not' b1) 'or' a1) . z) '&' ((('not' b2) 'or' a2) . z)) '&' ((b1 'or' b2) . z)) '&' (('not' (a1 '&' a2)) . z) by MARGREL1:def_20
.= ((((('not' b1) 'or' a1) . z) '&' ((('not' b2) 'or' a2) . z)) '&' ((b1 'or' b2) . z)) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:14
.= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) 'or' a2) . z)) '&' ((b1 'or' b2) . z)) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:def_4
.= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 'or' b2) . z)) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:def_4
.= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z))) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:def_4
.= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z))) '&' ((('not' a1) . z) 'or' (('not' a2) . z)) by BVFUNC_1:def_4 ;
assume  ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z <> TRUE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE
then A4: ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z))) '&' ((('not' a1) . z) 'or' (('not' a2) . z)) = FALSE by A3, XBOOLEAN:def_3;
now__::_thesis:_(_(_(((('not'_b1)_._z)_'or'_(a1_._z))_'&'_((('not'_b2)_._z)_'or'_(a2_._z)))_'&'_((b1_._z)_'or'_(b2_._z))_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_or_(_(('not'_a1)_._z)_'or'_(('not'_a2)_._z)_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_)
percases ( (((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z)) = FALSE or (('not' a1) . z) 'or' (('not' a2) . z) = FALSE ) by A4, MARGREL1:12;
caseA5: (((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z)) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE
now__::_thesis:_(_(_((('not'_b1)_._z)_'or'_(a1_._z))_'&'_((('not'_b2)_._z)_'or'_(a2_._z))_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_or_(_(b1_._z)_'or'_(b2_._z)_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_)
percases ( ((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z)) = FALSE or (b1 . z) 'or' (b2 . z) = FALSE ) by A5, MARGREL1:12;
caseA6: ((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z)) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE
now__::_thesis:_(_(_(('not'_b1)_._z)_'or'_(a1_._z)_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_or_(_(('not'_b2)_._z)_'or'_(a2_._z)_=_FALSE_&_((((b1_'imp'_a1)_'&'_(b2_'imp'_a2))_'&'_(b1_'or'_b2))_'&'_('not'_(a1_'&'_a2)))_._z_=_TRUE_)_)
percases ( (('not' b1) . z) 'or' (a1 . z) = FALSE or (('not' b2) . z) 'or' (a2 . z) = FALSE ) by A6, MARGREL1:12;
caseA7: (('not' b1) . z) 'or' (a1 . z) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE
A8: ( a1 . z = TRUE or a1 . z = FALSE ) by XBOOLEAN:def_3;
then  'not' (b1 . z) = FALSE by A7, MARGREL1:def_19;
then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = (((a2 . z) '&' ('not' (a2 . z))) 'or' ((a2 . z) '&' (b2 . z))) '&' ('not' (b2 . z)) by A7, A8, XBOOLEAN:8
.= (FALSE 'or' ((a2 . z) '&' (b2 . z))) '&' ('not' (b2 . z)) by XBOOLEAN:138
.= ((a2 . z) '&' (b2 . z)) '&' ('not' (b2 . z))
.= (a2 . z) '&' ((b2 . z) '&' ('not' (b2 . z)))
.= FALSE '&' (a2 . z) by XBOOLEAN:138
.= FALSE ;
hence  ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; ::_thesis: verum
end;
caseA9: (('not' b2) . z) 'or' (a2 . z) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE
A10: ( a2 . z = TRUE or a2 . z = FALSE ) by XBOOLEAN:def_3;
then  'not' (b2 . z) = FALSE by A9, MARGREL1:def_19;
then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = (((a1 . z) '&' ('not' (a1 . z))) 'or' ((a1 . z) '&' (b1 . z))) '&' ('not' (b1 . z)) by A9, A10, XBOOLEAN:8
.= (FALSE 'or' ((a1 . z) '&' (b1 . z))) '&' ('not' (b1 . z)) by XBOOLEAN:138
.= ((a1 . z) '&' (b1 . z)) '&' ('not' (b1 . z))
.= (a1 . z) '&' ((b1 . z) '&' ('not' (b1 . z)))
.= FALSE '&' (a1 . z) by XBOOLEAN:138
.= FALSE ;
hence  ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; ::_thesis: verum
end;
end;
end;
hence  ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; ::_thesis: verum
end;
caseA11: (b1 . z) 'or' (b2 . z) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE
reconsider a2z = a2 . z as boolean set ;
reconsider a1z = a1 . z as boolean set ;
 ( b1 . z = TRUE or b1 . z = FALSE ) by XBOOLEAN:def_3;
then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = ('not' (a1 . z)) '&' (('not' (a2 . z)) '&' ((a1 . z) 'or' (a2 . z))) by A11
.= ('not' (a1 . z)) '&' ((('not' (a2 . z)) '&' (a1 . z)) 'or' (('not' a2z) '&' a2z)) by XBOOLEAN:8
.= ('not' (a1 . z)) '&' ((('not' (a2 . z)) '&' (a1 . z)) 'or' FALSE) by XBOOLEAN:138
.= ('not' (a1 . z)) '&' ((a1 . z) '&' ('not' (a2 . z)))
.= (('not' a1z) '&' a1z) '&' ('not' (a2 . z))
.= FALSE '&' ('not' (a2 . z)) by XBOOLEAN:138
.= FALSE ;
hence  ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; ::_thesis: verum
end;
end;
end;
hence  ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; ::_thesis: verum
end;
caseA12: (('not' a1) . z) 'or' (('not' a2) . z) = FALSE ; ::_thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE
 ( ('not' a2) . z = TRUE or ('not' a2) . z = FALSE ) by XBOOLEAN:def_3;
then  ( 'not' (a1 . z) = FALSE & 'not' (a2 . z) = FALSE ) by A12, MARGREL1:def_19;
then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = (b1 . z) '&' ((b2 . z) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))))
.= (b1 . z) '&' (((b2 . z) '&' ('not' (b1 . z))) 'or' ((b2 . z) '&' ('not' (b2 . z)))) by XBOOLEAN:8
.= (b1 . z) '&' (((b2 . z) '&' ('not' (b1 . z))) 'or' FALSE) by XBOOLEAN:138
.= (b1 . z) '&' (('not' (b1 . z)) '&' (b2 . z))
.= ((b1 . z) '&' ('not' (b1 . z))) '&' (b2 . z)
.= FALSE '&' (b2 . z) by XBOOLEAN:138
.= FALSE ;
hence  ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; ::_thesis: verum
end;
end;
end;
hence  ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; ::_thesis: verum
end;
hence  ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC10:7
for Y being non empty set
for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) = (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))
proof
let Y be non empty set ; ::_thesis: for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) = (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))
let a1, a2, b1, b2 be Function of Y,BOOLEAN; ::_thesis: (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) = (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))
 ( (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) & (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) '<' (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) ) by Lm3;
hence  (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) = (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2)) by BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC10:8
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a 'or' b) '&' (c 'or' d) = (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d)
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds (a 'or' b) '&' (c 'or' d) = (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d)
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: (a 'or' b) '&' (c 'or' d) = (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d)
(a 'or' b) '&' (c 'or' d) = ((a 'or' b) '&' c) 'or' ((a 'or' b) '&' d) by BVFUNC_1:12
.= ((a '&' c) 'or' (b '&' c)) 'or' ((a 'or' b) '&' d) by BVFUNC_1:12
.= ((a '&' c) 'or' (b '&' c)) 'or' ((a '&' d) 'or' (b '&' d)) by BVFUNC_1:12
.= (((a '&' c) 'or' (b '&' c)) 'or' (a '&' d)) 'or' (b '&' d) by BVFUNC_1:8
.= (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d) by BVFUNC_1:8 ;
hence  (a 'or' b) '&' (c 'or' d) = (((a '&' c) 'or' (a '&' d)) 'or' (b '&' c)) 'or' (b '&' d) ; ::_thesis: verum
end;

theorem :: BVFUNC10:9
for Y being non empty set
for a1, a2, b1, b2, b3 being Function of Y,BOOLEAN holds (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3)
proof
let Y be non empty set ; ::_thesis: for a1, a2, b1, b2, b3 being Function of Y,BOOLEAN holds (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3)
let a1, a2, b1, b2, b3 be Function of Y,BOOLEAN; ::_thesis: (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3)
(((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) = ((((a1 'or' (b1 '&' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) by BVFUNC_1:11
.= (((a1 'or' ((b1 '&' b2) '&' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) by BVFUNC_1:11
.= ((a1 'or' ((b1 '&' b2) '&' b3)) '&' ((a2 'or' b1) '&' (a2 'or' b2))) '&' (a2 'or' b3) by BVFUNC_1:4
.= (a1 'or' ((b1 '&' b2) '&' b3)) '&' (((a2 'or' b1) '&' (a2 'or' b2)) '&' (a2 'or' b3)) by BVFUNC_1:4
.= (a1 'or' ((b1 '&' b2) '&' b3)) '&' ((a2 'or' (b1 '&' b2)) '&' (a2 'or' b3)) by BVFUNC_1:11
.= (a1 'or' ((b1 '&' b2) '&' b3)) '&' (a2 'or' ((b1 '&' b2) '&' b3)) by BVFUNC_1:11
.= (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) by BVFUNC_1:11 ;
hence  (a1 '&' a2) 'or' ((b1 '&' b2) '&' b3) = (((((a1 'or' b1) '&' (a1 'or' b2)) '&' (a1 'or' b3)) '&' (a2 'or' b1)) '&' (a2 'or' b2)) '&' (a2 'or' b3) ; ::_thesis: verum
end;

theorem :: BVFUNC10:10
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d)
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d)
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d)
A1: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = (((a 'imp' b) '&' (b 'imp' c)) '&' (a 'imp' c)) '&' (c 'imp' d) by BVFUNC_7:12
.= ((a 'imp' b) '&' (b 'imp' c)) '&' ((a 'imp' c) '&' (c 'imp' d)) by BVFUNC_1:4
.= ((a 'imp' b) '&' (b 'imp' c)) '&' (((a 'imp' c) '&' (c 'imp' d)) '&' (a 'imp' d)) by BVFUNC_7:12
.= (((a 'imp' b) '&' (b 'imp' c)) '&' ((a 'imp' c) '&' (c 'imp' d))) '&' (a 'imp' d) by BVFUNC_1:4
.= ((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4
.= (((a 'imp' b) '&' ((b 'imp' c) '&' (c 'imp' d))) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4
.= (((a 'imp' b) '&' (((b 'imp' c) '&' (c 'imp' d)) '&' (b 'imp' d))) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_7:12
.= ((((a 'imp' b) '&' ((b 'imp' c) '&' (c 'imp' d))) '&' (b 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (b 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d) by BVFUNC_1:4
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (b 'imp' d)) '&' (a 'imp' d) by BVFUNC_1:4
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d)) '&' (b 'imp' d) by BVFUNC_1:4 ;
((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) = ((('not' a) 'or' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) by BVFUNC_4:8
.= ((('not' a) 'or' ((b '&' c) '&' d)) '&' (('not' b) 'or' (c '&' d))) '&' (c 'imp' d) by BVFUNC_4:8
.= ((('not' a) 'or' ((b '&' c) '&' d)) '&' (('not' b) 'or' (c '&' d))) '&' (('not' c) 'or' d) by BVFUNC_4:8
.= ((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' (c '&' d))) '&' (('not' c) 'or' d) by BVFUNC_5:39
.= ((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' ((('not' b) 'or' c) '&' (('not' b) 'or' d))) '&' (('not' c) 'or' d) by BVFUNC_1:11
.= (((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' c)) '&' (('not' b) 'or' d)) '&' (('not' c) 'or' d) by BVFUNC_1:4
.= (((((('not' a) 'or' b) '&' (('not' a) 'or' c)) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d)) '&' (('not' c) 'or' d) by BVFUNC_1:4
.= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d)) '&' (('not' c) 'or' d) by BVFUNC_1:4
.= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' c) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_1:4
.= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' a) 'or' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_1:4
.= (((((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_1:4
.= (((((a 'imp' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (('not' c) 'or' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (('not' a) 'or' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (('not' a) 'or' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d)) '&' (('not' b) 'or' d) by BVFUNC_4:8
.= (((((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d)) '&' (a 'imp' c)) '&' (a 'imp' d)) '&' (b 'imp' d) by BVFUNC_4:8 ;
hence  ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' d) = ((a 'imp' ((b '&' c) '&' d)) '&' (b 'imp' (c '&' d))) '&' (c 'imp' d) by A1; ::_thesis: verum
end;

theorem :: BVFUNC10:11
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b) '<' c 'or' d
proof
let Y be non empty set ; ::_thesis: for a, b, c, d being Function of Y,BOOLEAN holds ((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b) '<' c 'or' d
let a, b, c, d be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b) '<' c 'or' d
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not (((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b)) . z = TRUE or (c 'or' d) . z = TRUE )
A1: (((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b)) . z = (((a 'imp' c) '&' (b 'imp' d)) . z) '&' ((a 'or' b) . z) by MARGREL1:def_20
.= (((a 'imp' c) . z) '&' ((b 'imp' d) . z)) '&' ((a 'or' b) . z) by MARGREL1:def_20
.= (((('not' a) 'or' c) . z) '&' ((b 'imp' d) . z)) '&' ((a 'or' b) . z) by BVFUNC_4:8
.= (((('not' a) 'or' c) . z) '&' ((('not' b) 'or' d) . z)) '&' ((a 'or' b) . z) by BVFUNC_4:8
.= (((('not' a) . z) 'or' (c . z)) '&' ((('not' b) 'or' d) . z)) '&' ((a 'or' b) . z) by BVFUNC_1:def_4
.= (((('not' a) . z) 'or' (c . z)) '&' ((('not' b) . z) 'or' (d . z))) '&' ((a 'or' b) . z) by BVFUNC_1:def_4
.= (((('not' a) . z) 'or' (c . z)) '&' ((('not' b) . z) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) by BVFUNC_1:def_4
.= ((('not' (a . z)) 'or' (c . z)) '&' ((('not' b) . z) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) by MARGREL1:def_19
.= ((('not' (a . z)) 'or' (c . z)) '&' (('not' (b . z)) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) by MARGREL1:def_19 ;
reconsider bz = b . z as boolean set ;
reconsider az = a . z as boolean set ;
assume A2: (((a 'imp' c) '&' (b 'imp' d)) '&' (a 'or' b)) . z = TRUE ; ::_thesis: (c 'or' d) . z = TRUE
now__::_thesis:_(_(c_'or'_d)_._z_<>_TRUE_implies_(c_'or'_d)_._z_=_TRUE_)
assume  (c 'or' d) . z <> TRUE ; ::_thesis: (c 'or' d) . z = TRUE
then  (c 'or' d) . z = FALSE by XBOOLEAN:def_3;
then A3: (c . z) 'or' (d . z) = FALSE by BVFUNC_1:def_4;
 ( d . z = TRUE or d . z = FALSE ) by XBOOLEAN:def_3;
then ((('not' (a . z)) 'or' (c . z)) '&' (('not' (b . z)) 'or' (d . z))) '&' ((a . z) 'or' (b . z)) = ('not' (a . z)) '&' (('not' (b . z)) '&' ((b . z) 'or' (a . z))) by A3
.= ('not' (a . z)) '&' ((('not' bz) '&' bz) 'or' (('not' (b . z)) '&' (a . z))) by XBOOLEAN:8
.= ('not' (a . z)) '&' (FALSE 'or' (('not' (b . z)) '&' (a . z))) by XBOOLEAN:138
.= ('not' (a . z)) '&' ((a . z) '&' ('not' (b . z)))
.= (('not' az) '&' az) '&' ('not' (b . z))
.= FALSE '&' ('not' (b . z)) by XBOOLEAN:138
.= FALSE ;
hence  (c 'or' d) . z = TRUE by A2, A1; ::_thesis: verum
end;
hence  (c 'or' d) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC10:12
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((a '&' b) 'imp' ('not' c)) '&' a) '&' c '<' 'not' b
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (((a '&' b) 'imp' ('not' c)) '&' a) '&' c '<' 'not' b
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (((a '&' b) 'imp' ('not' c)) '&' a) '&' c '<' 'not' b
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((((a '&' b) 'imp' ('not' c)) '&' a) '&' c) . z = TRUE or ('not' b) . z = TRUE )
A1: ((((a '&' b) 'imp' ('not' c)) '&' a) '&' c) . z = ((((a '&' b) 'imp' ('not' c)) '&' a) . z) '&' (c . z) by MARGREL1:def_20
.= ((((a '&' b) 'imp' ('not' c)) . z) '&' (a . z)) '&' (c . z) by MARGREL1:def_20
.= (((('not' (a '&' b)) 'or' ('not' c)) . z) '&' (a . z)) '&' (c . z) by BVFUNC_4:8
.= ((((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) '&' (a . z)) '&' (c . z) by BVFUNC_1:14
.= ((((('not' a) 'or' ('not' b)) . z) 'or' (('not' c) . z)) '&' (a . z)) '&' (c . z) by BVFUNC_1:def_4
.= ((((('not' a) . z) 'or' (('not' b) . z)) 'or' (('not' c) . z)) '&' (a . z)) '&' (c . z) by BVFUNC_1:def_4 ;
reconsider cz = c . z as boolean set ;
assume A2: ((((a '&' b) 'imp' ('not' c)) '&' a) '&' c) . z = TRUE ; ::_thesis: ('not' b) . z = TRUE
now__::_thesis:_(_('not'_b)_._z_<>_TRUE_implies_('not'_b)_._z_=_TRUE_)
assume  ('not' b) . z <> TRUE ; ::_thesis: ('not' b) . z = TRUE
then  ('not' b) . z = FALSE by XBOOLEAN:def_3;
then ((((('not' a) . z) 'or' (('not' b) . z)) 'or' (('not' c) . z)) '&' (a . z)) '&' (c . z) = ((('not' (a . z)) 'or' (('not' c) . z)) '&' (a . z)) '&' (c . z) by MARGREL1:def_19
.= ((a . z) '&' (('not' (a . z)) 'or' ('not' (c . z)))) '&' (c . z) by MARGREL1:def_19
.= (((a . z) '&' ('not' (a . z))) 'or' ((a . z) '&' ('not' (c . z)))) '&' (c . z) by XBOOLEAN:8
.= (FALSE 'or' ((a . z) '&' ('not' (c . z)))) '&' (c . z) by XBOOLEAN:138
.= ((a . z) '&' ('not' (c . z))) '&' (c . z)
.= (a . z) '&' (('not' cz) '&' cz)
.= FALSE '&' (a . z) by XBOOLEAN:138
.= FALSE ;
hence  ('not' b) . z = TRUE by A2, A1; ::_thesis: verum
end;
hence  ('not' b) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC10:13
for Y being non empty set
for a1, a2, a3, b1, b2, b3 being Function of Y,BOOLEAN holds ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3)
proof
let Y be non empty set ; ::_thesis: for a1, a2, a3, b1, b2, b3 being Function of Y,BOOLEAN holds ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3)
let a1, a2, a3, b1, b2, b3 be Function of Y,BOOLEAN; ::_thesis: ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3)
((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3) = ('not' ((('not' b1) '&' ('not' b2)) '&' a3)) 'or' ((('not' a1) 'or' ('not' a2)) 'or' b3) by BVFUNC_4:8
.= ((('not' ('not' b1)) 'or' ('not' ('not' b2))) 'or' ('not' a3)) 'or' ((('not' a1) 'or' ('not' a2)) 'or' b3) by BVFUNC_5:37
.= (((b1 'or' b2) 'or' ('not' a3)) 'or' (('not' a1) 'or' ('not' a2))) 'or' b3 by BVFUNC_1:8
.= ((b1 'or' b2) 'or' ((('not' a1) 'or' ('not' a2)) 'or' ('not' a3))) 'or' b3 by BVFUNC_1:8
.= ((('not' a1) 'or' ('not' a2)) 'or' ('not' a3)) 'or' ((b1 'or' b2) 'or' b3) by BVFUNC_1:8
.= ('not' ((a1 '&' a2) '&' a3)) 'or' ((b1 'or' b2) 'or' b3) by BVFUNC_5:37
.= ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) by BVFUNC_4:8 ;
hence  ((a1 '&' a2) '&' a3) 'imp' ((b1 'or' b2) 'or' b3) = ((('not' b1) '&' ('not' b2)) '&' a3) 'imp' ((('not' a1) 'or' ('not' a2)) 'or' b3) ; ::_thesis: verum
end;

theorem :: BVFUNC10:14
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))
 for z being Element of Y st (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE holds
(((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
proof
let z be Element of Y; ::_thesis: ( (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE implies (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE )
A1: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = (((a 'imp' b) '&' (b 'imp' c)) . z) '&' ((c 'imp' a) . z) by MARGREL1:def_20
.= (((a 'imp' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by MARGREL1:def_20
.= (((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8
.= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8
.= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_4:8
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def_4
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def_4
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by BVFUNC_1:def_4
.= ((('not' (a . z)) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def_19
.= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def_19
.= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' (('not' (c . z)) 'or' (a . z)) by MARGREL1:def_19 ;
assume A2: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
now__::_thesis:_(_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_<>_TRUE_implies_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)
A3: ( (('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z)) = TRUE or (('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z)) = FALSE ) by XBOOLEAN:def_3;
assume A4: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z <> TRUE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
A5: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = (((a '&' b) '&' c) . z) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by BVFUNC_1:def_4
.= (((a '&' b) . z) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) . z) '&' (('not' c) . z)) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) . z) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def_19
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' (('not' c) . z)) by MARGREL1:def_19
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z))) by MARGREL1:def_19 ;
A6: ( ((a . z) '&' (b . z)) '&' (c . z) = TRUE or ((a . z) '&' (b . z)) '&' (c . z) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_(a_._z)_'&'_(b_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_)
percases ( (a . z) '&' (b . z) = FALSE or c . z = FALSE ) by A4, A5, A6, MARGREL1:12;
caseA7: (a . z) '&' (b . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
now__::_thesis:_(_(_a_._z_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_or_(_b_._z_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_)
percases ( a . z = FALSE or b . z = FALSE ) by A7, MARGREL1:12;
caseA8: a . z = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
now__::_thesis:_(_(_'not'_(b_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_or_(_'not'_(c_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_)
percases ( 'not' (b . z) = FALSE or 'not' (c . z) = FALSE ) by A4, A5, A3, A8, MARGREL1:12;
case 'not' (b . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A8, XBOOLEAN:138; ::_thesis: verum
end;
case 'not' (c . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A8; ::_thesis: verum
end;
end;
end;
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
caseA9: b . z = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
now__::_thesis:_(_(_'not'_(a_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_or_(_'not'_(c_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_)
percases ( 'not' (a . z) = FALSE or 'not' (c . z) = FALSE ) by A4, A5, A3, A9, MARGREL1:12;
case 'not' (a . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A9; ::_thesis: verum
end;
case 'not' (c . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A9, XBOOLEAN:138; ::_thesis: verum
end;
end;
end;
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
caseA10: c . z = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
now__::_thesis:_(_(_'not'_(a_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_or_(_'not'_(b_._z)_=_FALSE_&_(((a_'&'_b)_'&'_c)_'or'_((('not'_a)_'&'_('not'_b))_'&'_('not'_c)))_._z_=_TRUE_)_)
percases ( 'not' (a . z) = FALSE or 'not' (b . z) = FALSE ) by A4, A5, A3, A10, MARGREL1:12;
case 'not' (a . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A10, XBOOLEAN:138; ::_thesis: verum
end;
case 'not' (b . z) = FALSE ; ::_thesis: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE by A2, A1, A10; ::_thesis: verum
end;
end;
end;
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
hence  (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
then A11: ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) '<' ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) by BVFUNC_1:def_12;
 for z being Element of Y st (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE holds
(((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
proof
let z be Element of Y; ::_thesis: ( (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE implies (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE )
A12: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = (((a '&' b) '&' c) . z) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by BVFUNC_1:def_4
.= (((a '&' b) . z) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) '&' ('not' c)) . z) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) '&' ('not' b)) . z) '&' (('not' c) . z)) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' (((('not' a) . z) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' (('not' b) . z)) '&' (('not' c) . z)) by MARGREL1:def_19
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' (('not' c) . z)) by MARGREL1:def_19
.= (((a . z) '&' (b . z)) '&' (c . z)) 'or' ((('not' (a . z)) '&' ('not' (b . z))) '&' ('not' (c . z))) by MARGREL1:def_19 ;
assume A13: (((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c))) . z = TRUE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
now__::_thesis:_(_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_<>_TRUE_implies_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_=_TRUE_)
A14: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = (((a 'imp' b) '&' (b 'imp' c)) . z) '&' ((c 'imp' a) . z) by MARGREL1:def_20
.= (((a 'imp' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by MARGREL1:def_20
.= (((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8
.= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((c 'imp' a) . z) by BVFUNC_4:8
.= (((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_4:8
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z)) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def_4
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) 'or' a) . z) by BVFUNC_1:def_4
.= (((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by BVFUNC_1:def_4
.= ((('not' (a . z)) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def_19
.= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' ((('not' c) . z) 'or' (a . z)) by MARGREL1:def_19
.= ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' (('not' (c . z)) 'or' (a . z)) by MARGREL1:def_19 ;
assume  (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z <> TRUE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
then A15: ((('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z))) '&' (('not' (c . z)) 'or' (a . z)) = FALSE by A14, XBOOLEAN:def_3;
now__::_thesis:_(_(_(('not'_(a_._z))_'or'_(b_._z))_'&'_(('not'_(b_._z))_'or'_(c_._z))_=_FALSE_&_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_=_TRUE_)_or_(_('not'_(c_._z))_'or'_(a_._z)_=_FALSE_&_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_=_TRUE_)_)
percases ( (('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z)) = FALSE or ('not' (c . z)) 'or' (a . z) = FALSE ) by A15, MARGREL1:12;
caseA16: (('not' (a . z)) 'or' (b . z)) '&' (('not' (b . z)) 'or' (c . z)) = FALSE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
now__::_thesis:_(_(_('not'_(a_._z))_'or'_(b_._z)_=_FALSE_&_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_=_TRUE_)_or_(_('not'_(b_._z))_'or'_(c_._z)_=_FALSE_&_(((a_'imp'_b)_'&'_(b_'imp'_c))_'&'_(c_'imp'_a))_._z_=_TRUE_)_)
percases ( ('not' (a . z)) 'or' (b . z) = FALSE or ('not' (b . z)) 'or' (c . z) = FALSE ) by A16, MARGREL1:12;
caseA17: ('not' (a . z)) 'or' (b . z) = FALSE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
 ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3;
hence  (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE by A13, A12, A17; ::_thesis: verum
end;
caseA18: ('not' (b . z)) 'or' (c . z) = FALSE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
 ( c . z = TRUE or c . z = FALSE ) by XBOOLEAN:def_3;
hence  (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE by A13, A12, A18; ::_thesis: verum
end;
end;
end;
hence  (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; ::_thesis: verum
end;
caseA19: ('not' (c . z)) 'or' (a . z) = FALSE ; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE
 ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3;
hence  (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE by A13, A12, A19; ::_thesis: verum
end;
end;
end;
hence  (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; ::_thesis: verum
end;
hence  (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) . z = TRUE ; ::_thesis: verum
end;
then  ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) '<' ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) by BVFUNC_1:def_12;
hence  ((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a) = ((a '&' b) '&' c) 'or' ((('not' a) '&' ('not' b)) '&' ('not' c)) by A11, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC10:15
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (a '&' b) '&' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (a '&' b) '&' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (a '&' b) '&' c
(((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (((('not' a) 'or' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) by BVFUNC_4:8
.= (((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) by BVFUNC_4:8
.= (((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (('not' c) 'or' a)) '&' ((a 'or' b) 'or' c) by BVFUNC_4:8
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((('not' c) 'or' a) '&' ((a 'or' b) 'or' c)) by BVFUNC_1:4
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (((('not' c) 'or' a) '&' (a 'or' b)) 'or' ((('not' c) 'or' a) '&' c)) by BVFUNC_1:12
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (((('not' c) 'or' a) '&' (a 'or' b)) 'or' ((('not' c) '&' c) 'or' (a '&' c))) by BVFUNC_1:12
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (((('not' c) 'or' a) '&' (a 'or' b)) 'or' ((O_el Y) 'or' (a '&' c))) by BVFUNC_4:5
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (((('not' c) 'or' a) '&' (a 'or' b)) 'or' (a '&' c)) by BVFUNC_1:9
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((a 'or' (('not' c) '&' b)) 'or' (a '&' c)) by BVFUNC_1:11
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((a 'or' (a '&' c)) 'or' (('not' c) '&' b)) by BVFUNC_1:8
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (((a '&' (I_el Y)) 'or' (a '&' c)) 'or' (('not' c) '&' b)) by BVFUNC_1:6
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((a '&' ((I_el Y) 'or' c)) 'or' (('not' c) '&' b)) by BVFUNC_1:12
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((a '&' (I_el Y)) 'or' (('not' c) '&' b)) by BVFUNC_1:10
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' (a 'or' (('not' c) '&' b)) by BVFUNC_1:6
.= ((('not' a) 'or' b) '&' (('not' b) 'or' c)) '&' ((a 'or' ('not' c)) '&' (a 'or' b)) by BVFUNC_1:11
.= ((a 'or' b) '&' ((('not' a) 'or' b) '&' (('not' b) 'or' c))) '&' (a 'or' ('not' c)) by BVFUNC_1:4
.= (((a 'or' b) '&' (('not' a) 'or' b)) '&' (('not' b) 'or' c)) '&' (a 'or' ('not' c)) by BVFUNC_1:4
.= (((a '&' ('not' a)) 'or' b) '&' (('not' b) 'or' c)) '&' (a 'or' ('not' c)) by BVFUNC_1:11
.= (((O_el Y) 'or' b) '&' (('not' b) 'or' c)) '&' (a 'or' ('not' c)) by BVFUNC_4:5
.= (b '&' (('not' b) 'or' c)) '&' (a 'or' ('not' c)) by BVFUNC_1:9
.= ((b '&' ('not' b)) 'or' (b '&' c)) '&' (a 'or' ('not' c)) by BVFUNC_1:12
.= ((O_el Y) 'or' (b '&' c)) '&' (a 'or' ('not' c)) by BVFUNC_4:5
.= (b '&' c) '&' (a 'or' ('not' c)) by BVFUNC_1:9
.= ((b '&' c) '&' a) 'or' ((b '&' c) '&' ('not' c)) by BVFUNC_1:12
.= ((b '&' c) '&' a) 'or' (b '&' (c '&' ('not' c))) by BVFUNC_1:4
.= ((b '&' c) '&' a) 'or' (b '&' (O_el Y)) by BVFUNC_4:5
.= ((b '&' c) '&' a) 'or' (O_el Y) by BVFUNC_1:5
.= (b '&' c) '&' a by BVFUNC_1:9
.= (a '&' b) '&' c by BVFUNC_1:4 ;
hence  (((a 'imp' b) '&' (b 'imp' c)) '&' (c 'imp' a)) '&' ((a 'or' b) 'or' c) = (a '&' b) '&' c ; ::_thesis: verum
end;

Lm4:  for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE or ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE )
A1: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) . z) 'or' (((a '&' b) '&' ('not' c)) . z) by BVFUNC_1:def_4
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) '&' ('not' c)) . z) by BVFUNC_1:def_4
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) . z) '&' (('not' c) . z)) by MARGREL1:def_20
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) . z) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= ((((('not' a) '&' b) . z) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= ((((('not' a) . z) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_19
.= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_19
.= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' ('not' (c . z))) by MARGREL1:def_19 ;
assume A2: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE
now__::_thesis:_(_((a_'or'_b)_'&'_('not'_((a_'&'_b)_'&'_c)))_._z_<>_TRUE_implies_((a_'or'_b)_'&'_('not'_((a_'&'_b)_'&'_c)))_._z_=_TRUE_)
A3: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = ((a 'or' b) '&' ((('not' a) 'or' ('not' b)) 'or' ('not' c))) . z by BVFUNC_5:37
.= ((a 'or' b) . z) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by MARGREL1:def_20
.= ((a . z) 'or' (b . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def_4
.= ((a . z) 'or' (b . z)) '&' (((('not' a) 'or' ('not' b)) . z) 'or' (('not' c) . z)) by BVFUNC_1:def_4
.= ((a . z) 'or' (b . z)) '&' (((('not' a) . z) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by BVFUNC_1:def_4
.= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by MARGREL1:def_19
.= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' (('not' c) . z)) by MARGREL1:def_19
.= ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z))) by MARGREL1:def_19 ;
assume  ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z <> TRUE ; ::_thesis: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE
then A4: ((a . z) 'or' (b . z)) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z))) = FALSE by A3, XBOOLEAN:def_3;
now__::_thesis:_(_(_(a_._z)_'or'_(b_._z)_=_FALSE_&_((a_'or'_b)_'&'_('not'_((a_'&'_b)_'&'_c)))_._z_=_TRUE_)_or_(_(('not'_(a_._z))_'or'_('not'_(b_._z)))_'or'_('not'_(c_._z))_=_FALSE_&_((a_'or'_b)_'&'_('not'_((a_'&'_b)_'&'_c)))_._z_=_TRUE_)_)
percases ( (a . z) 'or' (b . z) = FALSE or (('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z)) = FALSE ) by A4, MARGREL1:12;
caseA5: (a . z) 'or' (b . z) = FALSE ; ::_thesis: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE
 ( b . z = TRUE or b . z = FALSE ) by XBOOLEAN:def_3;
hence  ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE by A2, A1, A5; ::_thesis: verum
end;
caseA6: (('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z)) = FALSE ; ::_thesis: ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE
A7: ( 'not' (b . z) = TRUE or 'not' (b . z) = FALSE ) by XBOOLEAN:def_3;
 ( ('not' (a . z)) 'or' ('not' (b . z)) = TRUE or ('not' (a . z)) 'or' ('not' (b . z)) = FALSE ) by XBOOLEAN:def_3;
hence  ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE by A2, A1, A6, A7; ::_thesis: verum
end;
end;
end;
hence  ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE ; ::_thesis: verum
end;
hence  ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC10:16
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))
A1: (((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' ((c 'or' a) '&' ('not' ((a '&' b) '&' c))) = ((((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4
.= ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4
.= (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' (('not' ((a '&' b) '&' c)) '&' ('not' ((a '&' b) '&' c))) by BVFUNC_1:4
.= (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) ;
 for z being Element of Y st ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = TRUE holds
((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
proof
let z be Element of Y; ::_thesis: ( ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = TRUE implies ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE )
A2: ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) . z) '&' (('not' ((a '&' b) '&' c)) . z) by MARGREL1:def_20
.= ((((a 'or' b) '&' (b 'or' c)) . z) '&' ((c 'or' a) . z)) '&' (('not' ((a '&' b) '&' c)) . z) by MARGREL1:def_20
.= ((((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z)) '&' (('not' ((a '&' b) '&' c)) . z) by MARGREL1:def_20
.= ((((a 'or' b) . z) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_5:37
.= ((((a . z) 'or' (b . z)) '&' ((b 'or' c) . z)) '&' ((c 'or' a) . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def_4
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c 'or' a) . z)) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def_4
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' (((('not' a) 'or' ('not' b)) 'or' ('not' c)) . z) by BVFUNC_1:def_4
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' (((('not' a) 'or' ('not' b)) . z) 'or' (('not' c) . z)) by BVFUNC_1:def_4
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' (((('not' a) . z) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by BVFUNC_1:def_4
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' ((('not' (a . z)) 'or' (('not' b) . z)) 'or' (('not' c) . z)) by MARGREL1:def_19
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' (('not' c) . z)) by MARGREL1:def_19
.= ((((a . z) 'or' (b . z)) '&' ((b . z) 'or' (c . z))) '&' ((c . z) 'or' (a . z))) '&' ((('not' (a . z)) 'or' ('not' (b . z))) 'or' ('not' (c . z))) by MARGREL1:def_19 ;
assume A3: ((((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c))) . z = TRUE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
now__::_thesis:_(_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_<>_TRUE_implies_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)
A4: ( ((a . z) '&' (b . z)) '&' ('not' (c . z)) = TRUE or ((a . z) '&' (b . z)) '&' ('not' (c . z)) = FALSE ) by XBOOLEAN:def_3;
assume A5: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z <> TRUE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
A6: ( ((a . z) '&' ('not' (b . z))) '&' (c . z) = TRUE or ((a . z) '&' ('not' (b . z))) '&' (c . z) = FALSE ) by XBOOLEAN:def_3;
A7: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) . z) 'or' (((a '&' b) '&' ('not' c)) . z) by BVFUNC_1:def_4
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) '&' ('not' c)) . z) by BVFUNC_1:def_4
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a '&' b) . z) '&' (('not' c) . z)) by MARGREL1:def_20
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) '&' c) . z)) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a '&' ('not' b)) . z) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= ((((('not' a) '&' b) '&' c) . z) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= ((((('not' a) '&' b) . z) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= ((((('not' a) . z) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_20
.= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' (('not' b) . z)) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_19
.= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' (('not' c) . z)) by MARGREL1:def_19
.= (((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z))) 'or' (((a . z) '&' (b . z)) '&' ('not' (c . z))) by MARGREL1:def_19 ;
A8: ( ((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z)) = TRUE or ((('not' (a . z)) '&' (b . z)) '&' (c . z)) 'or' (((a . z) '&' ('not' (b . z))) '&' (c . z)) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_('not'_(a_._z))_'&'_(b_._z)_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_)
percases ( ('not' (a . z)) '&' (b . z) = FALSE or c . z = FALSE ) by A5, A7, A8, A6, MARGREL1:12;
caseA9: ('not' (a . z)) '&' (b . z) = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
now__::_thesis:_(_(_'not'_(a_._z)_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_or_(_b_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_)
percases ( 'not' (a . z) = FALSE or b . z = FALSE ) by A9, MARGREL1:12;
caseA10: 'not' (a . z) = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
now__::_thesis:_(_(_'not'_(b_._z)_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_)
percases ( 'not' (b . z) = FALSE or c . z = FALSE ) by A5, A7, A6, A10, MARGREL1:12;
case 'not' (b . z) = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A7, A10; ::_thesis: verum
end;
case c . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A7, A10; ::_thesis: verum
end;
end;
end;
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
caseA11: b . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
now__::_thesis:_(_(_a_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_)
percases ( a . z = FALSE or c . z = FALSE ) by A5, A7, A6, A11, MARGREL1:12;
case a . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A11; ::_thesis: verum
end;
case c . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A11; ::_thesis: verum
end;
end;
end;
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
caseA12: c . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
now__::_thesis:_(_(_a_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_or_(_b_._z_=_FALSE_&_((((('not'_a)_'&'_b)_'&'_c)_'or'_((a_'&'_('not'_b))_'&'_c))_'or'_((a_'&'_b)_'&'_('not'_c)))_._z_=_TRUE_)_)
percases ( a . z = FALSE or b . z = FALSE ) by A5, A7, A4, A12, MARGREL1:12;
case a . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A12; ::_thesis: verum
end;
case b . z = FALSE ; ::_thesis: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE by A3, A2, A12; ::_thesis: verum
end;
end;
end;
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
end;
end;
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
hence  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) . z = TRUE ; ::_thesis: verum
end;
then A13: (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) '<' (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) by BVFUNC_1:def_12;
 (((('not' c) '&' a) '&' b) 'or' ((c '&' ('not' a)) '&' b)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((c '&' a) '&' b)) by Lm4;
then  (((('not' c) '&' a) '&' b) 'or' ((c '&' ('not' a)) '&' b)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then  (((a '&' b) '&' ('not' c)) 'or' ((c '&' ('not' a)) '&' b)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then  (((a '&' b) '&' ('not' c)) 'or' ((('not' a) '&' b) '&' c)) 'or' ((c '&' a) '&' ('not' b)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then  (((a '&' b) '&' ('not' c)) 'or' ((('not' a) '&' b) '&' c)) 'or' ((a '&' ('not' b)) '&' c) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then  (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (c 'or' a) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:8;
then A14: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((c 'or' a) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:16;
 (((('not' b) '&' c) '&' a) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((b '&' c) '&' ('not' a)) '<' (b 'or' c) '&' ('not' ((b '&' c) '&' a)) by Lm4;
then  (((('not' b) '&' c) '&' a) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((b '&' c) '&' ('not' a)) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then  (((('not' b) '&' c) '&' a) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((('not' a) '&' b) '&' c) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then  (((a '&' ('not' b)) '&' c) 'or' ((b '&' ('not' c)) '&' a)) 'or' ((('not' a) '&' b) '&' c) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then  (((a '&' ('not' b)) '&' c) 'or' ((a '&' b) '&' ('not' c))) 'or' ((('not' a) '&' b) '&' c) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:4;
then  (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (b 'or' c) '&' ('not' ((a '&' b) '&' c)) by BVFUNC_1:8;
then A15: ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((b 'or' c) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:16;
 (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (a 'or' b) '&' ('not' ((a '&' b) '&' c)) by Lm4;
then  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((a 'or' b) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:16;
then  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' (((a 'or' b) '&' ('not' ((a '&' b) '&' c))) '&' ((b 'or' c) '&' ('not' ((a '&' b) '&' c)))) = I_el Y by A15, BVFUNC_6:18;
then  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((((a 'or' b) '&' ('not' ((a '&' b) '&' c))) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:4;
then  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' ('not' ((a '&' b) '&' c))) = I_el Y by BVFUNC_1:4;
then  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' (((a 'or' b) '&' (b 'or' c)) '&' (('not' ((a '&' b) '&' c)) '&' ('not' ((a '&' b) '&' c)))) = I_el Y by BVFUNC_1:4;
then  ((((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c))) 'imp' ((((a 'or' b) '&' (b 'or' c)) '&' ('not' ((a '&' b) '&' c))) '&' ((c 'or' a) '&' ('not' ((a '&' b) '&' c)))) = I_el Y by A14, BVFUNC_6:18;
then  (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) '<' (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) by A1, BVFUNC_1:16;
hence  (((a 'or' b) '&' (b 'or' c)) '&' (c 'or' a)) '&' ('not' ((a '&' b) '&' c)) = (((('not' a) '&' b) '&' c) 'or' ((a '&' ('not' b)) '&' c)) 'or' ((a '&' b) '&' ('not' c)) by A13, BVFUNC_1:15; ::_thesis: verum
end;

theorem :: BVFUNC10:17
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b '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) '&' (b 'imp' c) '<' a 'imp' (b '&' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b '&' c)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or (a 'imp' (b '&' c)) . z = TRUE )
A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20
.= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8
.= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ;
assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: (a 'imp' (b '&' c)) . z = TRUE
now__::_thesis:_(_(a_'imp'_(b_'&'_c))_._z_<>_TRUE_implies_(a_'imp'_(b_'&'_c))_._z_=_TRUE_)
A3: (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
.= ('not' (a . z)) 'or' ((b . z) '&' (c . z)) by MARGREL1:def_19 ;
assume A4: (a 'imp' (b '&' c)) . z <> TRUE ; ::_thesis: (a 'imp' (b '&' c)) . z = TRUE
 ( 'not' (a . z) = TRUE or 'not' (a . z) = FALSE ) by XBOOLEAN:def_3;
then A5: ('not' a) . z = FALSE by A4, A3, MARGREL1:def_19;
A6: ( (b . z) '&' (c . z) = TRUE or (b . z) '&' (c . z) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_b_._z_=_FALSE_&_(a_'imp'_(b_'&'_c))_._z_=_TRUE_)_or_(_c_._z_=_FALSE_&_(a_'imp'_(b_'&'_c))_._z_=_TRUE_)_)
percases ( b . z = FALSE or c . z = FALSE ) by A4, A3, A6, MARGREL1:12;
case b . z = FALSE ; ::_thesis: (a 'imp' (b '&' c)) . z = TRUE
hence  (a 'imp' (b '&' c)) . z = TRUE by A2, A1, A5; ::_thesis: verum
end;
case c . z = FALSE ; ::_thesis: (a 'imp' (b '&' c)) . z = TRUE
then ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) = (b . z) '&' ('not' (b . z)) by A5, MARGREL1:def_19
.= FALSE by XBOOLEAN:138 ;
hence  (a 'imp' (b '&' c)) . z = TRUE by A2, A1; ::_thesis: verum
end;
end;
end;
hence  (a 'imp' (b '&' c)) . z = TRUE ; ::_thesis: verum
end;
hence  (a 'imp' (b '&' c)) . z = TRUE ; ::_thesis: verum
end;

theorem :: BVFUNC10:18
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' (a 'or' b) 'imp' c
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or ((a 'or' b) 'imp' c) . z = TRUE )
A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20
.= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8
.= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ;
assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: ((a 'or' b) 'imp' c) . z = TRUE
now__::_thesis:_(_((a_'or'_b)_'imp'_c)_._z_<>_TRUE_implies_((a_'or'_b)_'imp'_c)_._z_=_TRUE_)
A3: ( c . z = TRUE or c . z = FALSE ) by XBOOLEAN:def_3;
assume A4: ((a 'or' b) 'imp' c) . z <> TRUE ; ::_thesis: ((a 'or' b) 'imp' c) . z = TRUE
A5: ((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 ;
A6: ( (('not' a) . z) '&' (('not' b) . z) = TRUE or (('not' a) . z) '&' (('not' b) . z) = FALSE ) by XBOOLEAN:def_3;
now__::_thesis:_(_(_('not'_a)_._z_=_FALSE_&_((a_'or'_b)_'imp'_c)_._z_=_TRUE_)_or_(_('not'_b)_._z_=_FALSE_&_((a_'or'_b)_'imp'_c)_._z_=_TRUE_)_)
percases ( ('not' a) . z = FALSE or ('not' b) . z = FALSE ) by A4, A5, A6, MARGREL1:12;
case ('not' a) . z = FALSE ; ::_thesis: ((a 'or' b) 'imp' c) . z = TRUE
then ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) = (b . z) '&' ('not' (b . z)) by A4, A5, A3, MARGREL1:def_19
.= FALSE by XBOOLEAN:138 ;
hence  ((a 'or' b) 'imp' c) . z = TRUE by A2, A1; ::_thesis: verum
end;
case ('not' b) . z = FALSE ; ::_thesis: ((a 'or' b) 'imp' c) . z = TRUE
then ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) = ((('not' a) . z) 'or' (b . z)) '&' FALSE by A4, A5, XBOOLEAN:def_3
.= FALSE ;
hence  ((a 'or' b) 'imp' c) . z = TRUE by A2, A1; ::_thesis: verum
end;
end;
end;
hence  ((a 'or' b) 'imp' c) . z = TRUE ; ::_thesis: verum
end;
hence  ((a 'or' b) 'imp' c) . z = TRUE ; ::_thesis: verum
end;

theorem Th19: :: BVFUNC10:19
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b '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) '&' (b 'imp' c) '<' a 'imp' (b 'or' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' c)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or (a 'imp' (b 'or' c)) . z = TRUE )
A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20
.= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8
.= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ;
assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: (a 'imp' (b 'or' c)) . z = TRUE
now__::_thesis:_(_(a_'imp'_(b_'or'_c))_._z_<>_TRUE_implies_(a_'imp'_(b_'or'_c))_._z_=_TRUE_)
assume  (a 'imp' (b 'or' c)) . z <> TRUE ; ::_thesis: (a 'imp' (b 'or' c)) . z = TRUE
A3: ( ('not' a) . z = TRUE or ('not' a) . z = FALSE ) by XBOOLEAN:def_3;
A4: ( (b . z) 'or' (c . z) = TRUE or (b . z) 'or' (c . z) = FALSE ) by XBOOLEAN:def_3;
A5: ( c . z = TRUE or c . z = FALSE ) by XBOOLEAN:def_3;
(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 ;
hence  (a 'imp' (b 'or' c)) . z = TRUE by A2, A1, A3, A4, A5; ::_thesis: verum
end;
hence  (a 'imp' (b 'or' c)) . z = TRUE ; ::_thesis: verum
end;

theorem Th20: :: BVFUNC10:20
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or (a 'imp' (b 'or' ('not' c))) . z = TRUE )
A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20
.= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8
.= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ;
assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: (a 'imp' (b 'or' ('not' c))) . z = TRUE
now__::_thesis:_(_(a_'imp'_(b_'or'_('not'_c)))_._z_<>_TRUE_implies_(a_'imp'_(b_'or'_('not'_c)))_._z_=_TRUE_)
assume  (a 'imp' (b 'or' ('not' c))) . z <> TRUE ; ::_thesis: (a 'imp' (b 'or' ('not' c))) . z = TRUE
A3: ( ('not' a) . z = TRUE or ('not' a) . z = FALSE ) by XBOOLEAN:def_3;
A4: ( (b . z) 'or' (('not' c) . z) = TRUE or (b . z) 'or' (('not' c) . z) = FALSE ) by XBOOLEAN:def_3;
A5: ( ('not' c) . z = TRUE or ('not' c) . z = FALSE ) by XBOOLEAN:def_3;
(a 'imp' (b 'or' ('not' c))) . z = (('not' a) 'or' (b 'or' ('not' c))) . z by BVFUNC_4:8
.= (('not' a) . z) 'or' ((b 'or' ('not' c)) . z) by BVFUNC_1:def_4
.= (('not' a) . z) 'or' ((b . z) 'or' (('not' c) . z)) by BVFUNC_1:def_4 ;
hence  (a 'imp' (b 'or' ('not' c))) . z = TRUE by A2, A1, A3, A4, A5; ::_thesis: verum
end;
hence  (a 'imp' (b 'or' ('not' c))) . z = TRUE ; ::_thesis: verum
end;

theorem Th21: :: BVFUNC10:21
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a)
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or (b 'imp' (c 'or' a)) . z = TRUE )
A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20
.= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8
.= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ;
assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: (b 'imp' (c 'or' a)) . z = TRUE
now__::_thesis:_(_(b_'imp'_(c_'or'_a))_._z_<>_TRUE_implies_(b_'imp'_(c_'or'_a))_._z_=_TRUE_)
assume  (b 'imp' (c 'or' a)) . z <> TRUE ; ::_thesis: (b 'imp' (c 'or' a)) . z = TRUE
A3: ( ('not' b) . z = TRUE or ('not' b) . z = FALSE ) by XBOOLEAN:def_3;
A4: ( (c . z) 'or' (a . z) = TRUE or (c . z) 'or' (a . z) = FALSE ) by XBOOLEAN:def_3;
A5: ( a . z = TRUE or a . z = FALSE ) by XBOOLEAN:def_3;
(b 'imp' (c 'or' a)) . z = (('not' b) 'or' (c 'or' a)) . z by BVFUNC_4:8
.= (('not' b) . z) 'or' ((c 'or' a) . z) by BVFUNC_1:def_4
.= (('not' b) . z) 'or' ((c . z) 'or' (a . z)) by BVFUNC_1:def_4 ;
hence  (b 'imp' (c 'or' a)) . z = TRUE by A2, A1, A3, A4, A5; ::_thesis: verum
end;
hence  (b 'imp' (c 'or' a)) . z = TRUE ; ::_thesis: verum
end;

theorem Th22: :: BVFUNC10:22
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' ('not' a))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' ('not' a))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' ('not' a))
let z be Element of Y; :: according to BVFUNC_1:def_12 ::_thesis: ( not ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE or (b 'imp' (c 'or' ('not' a))) . z = TRUE )
A1: ((a 'imp' b) '&' (b 'imp' c)) . z = ((a 'imp' b) . z) '&' ((b 'imp' c) . z) by MARGREL1:def_20
.= ((('not' a) 'or' b) . z) '&' ((b 'imp' c) . z) by BVFUNC_4:8
.= ((('not' a) 'or' b) . z) '&' ((('not' b) 'or' c) . z) by BVFUNC_4:8
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) 'or' c) . z) by BVFUNC_1:def_4
.= ((('not' a) . z) 'or' (b . z)) '&' ((('not' b) . z) 'or' (c . z)) by BVFUNC_1:def_4 ;
assume A2: ((a 'imp' b) '&' (b 'imp' c)) . z = TRUE ; ::_thesis: (b 'imp' (c 'or' ('not' a))) . z = TRUE
now__::_thesis:_(_(b_'imp'_(c_'or'_('not'_a)))_._z_<>_TRUE_implies_(b_'imp'_(c_'or'_('not'_a)))_._z_=_TRUE_)
assume  (b 'imp' (c 'or' ('not' a))) . z <> TRUE ; ::_thesis: (b 'imp' (c 'or' ('not' a))) . z = TRUE
A3: ( ('not' b) . z = TRUE or ('not' b) . z = FALSE ) by XBOOLEAN:def_3;
A4: ( (c . z) 'or' (('not' a) . z) = TRUE or (c . z) 'or' (('not' a) . z) = FALSE ) by XBOOLEAN:def_3;
A5: ( ('not' a) . z = TRUE or ('not' a) . z = FALSE ) by XBOOLEAN:def_3;
(b 'imp' (c 'or' ('not' a))) . z = (('not' b) 'or' (c 'or' ('not' a))) . z by BVFUNC_4:8
.= (('not' b) . z) 'or' ((c 'or' ('not' a)) . z) by BVFUNC_1:def_4
.= (('not' b) . z) 'or' ((c . z) 'or' (('not' a) . z)) by BVFUNC_1:def_4 ;
hence  (b 'imp' (c 'or' ('not' a))) . z = TRUE by A2, A1, A3, A4, A5; ::_thesis: verum
end;
hence  (b 'imp' (c 'or' ('not' a))) . z = TRUE ; ::_thesis: verum
end;

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

theorem :: BVFUNC10:24
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' c)
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' c)
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' c)
 (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c)) by Th20;
then A1: ((a 'imp' b) '&' (b 'imp' c)) 'imp' (a 'imp' (b 'or' ('not' c))) = I_el Y by BVFUNC_1:16;
 ((a 'imp' b) '&' (b 'imp' c)) 'imp' (b 'imp' c) = I_el Y by BVFUNC_6:38;
then  ((a 'imp' b) '&' (b 'imp' c)) 'imp' ((a 'imp' (b 'or' ('not' c))) '&' (b 'imp' c)) = I_el Y by A1, BVFUNC_6:18;
hence  (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' c) by BVFUNC_1:16; ::_thesis: verum
end;

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

theorem :: BVFUNC10:26
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' a))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' a))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' a))
 (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' a) by Th21;
then A1: ((a 'imp' b) '&' (b 'imp' c)) 'imp' (b 'imp' (c 'or' a)) = I_el Y by BVFUNC_1:16;
 (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c)) by Th20;
then  ((a 'imp' b) '&' (b 'imp' c)) 'imp' (a 'imp' (b 'or' ('not' c))) = I_el Y by BVFUNC_1:16;
then  ((a 'imp' b) '&' (b 'imp' c)) 'imp' ((a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' a))) = I_el Y by A1, BVFUNC_6:18;
hence  (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' a)) by BVFUNC_1:16; ::_thesis: verum
end;

theorem :: BVFUNC10:27
for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' ('not' a)))
proof
let Y be non empty set ; ::_thesis: for a, b, c being Function of Y,BOOLEAN holds (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' ('not' a)))
let a, b, c be Function of Y,BOOLEAN; ::_thesis: (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' ('not' a)))
 (a 'imp' b) '&' (b 'imp' c) '<' b 'imp' (c 'or' ('not' a)) by Th22;
then A1: ((a 'imp' b) '&' (b 'imp' c)) 'imp' (b 'imp' (c 'or' ('not' a))) = I_el Y by BVFUNC_1:16;
 (a 'imp' b) '&' (b 'imp' c) '<' a 'imp' (b 'or' ('not' c)) by Th20;
then  ((a 'imp' b) '&' (b 'imp' c)) 'imp' (a 'imp' (b 'or' ('not' c))) = I_el Y by BVFUNC_1:16;
then  ((a 'imp' b) '&' (b 'imp' c)) 'imp' ((a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' ('not' a)))) = I_el Y by A1, BVFUNC_6:18;
hence  (a 'imp' b) '&' (b 'imp' c) '<' (a 'imp' (b 'or' ('not' c))) '&' (b 'imp' (c 'or' ('not' a))) by BVFUNC_1:16; ::_thesis: verum
end;