let Y be non empty set ; for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds ((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' a2 'imp' a1
let a1, b1, c1, a2, b2, c2 be Function of Y,BOOLEAN; ((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' a2 'imp' a1
A1:
((((b1 'or' c1) 'imp' (b2 'or' c2)) '&' ((b2 'or' c2) 'imp' ('not' a2))) '&' ((b1 'or' c1) 'imp' ('not' a2))) 'imp' ((b1 'or' c1) 'imp' ('not' a2)) = I_el Y
by Th38;
A2:
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (c1 'imp' c2) = I_el Y
by Lm4, BVFUNC_1:16;
A3:
((b1 'imp' b2) '&' (c1 'imp' c2)) 'imp' ((b1 'or' c1) 'imp' (b2 'or' c2)) = I_el Y
by Th21, BVFUNC_1:16;
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (b1 'imp' b2) = I_el Y
by Lm4, BVFUNC_1:16;
then
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ((b1 'imp' b2) '&' (c1 'imp' c2)) = I_el Y
by A2, th18;
then A4:
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ((b1 'or' c1) 'imp' (b2 'or' c2)) = I_el Y
by A3, BVFUNC_5:9;
A5:
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ('not' (a2 '&' c2)) = I_el Y
by Lm1, BVFUNC_1:16;
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ('not' (a2 '&' b2)) = I_el Y
by Lm2, BVFUNC_1:16;
then
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (('not' (a2 '&' b2)) '&' ('not' (a2 '&' c2))) = I_el Y
by A5, th18;
then A6:
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (((b1 'or' c1) 'imp' (b2 'or' c2)) '&' (('not' (a2 '&' b2)) '&' ('not' (a2 '&' c2)))) = I_el Y
by A4, th18;
('not' (a2 '&' b2)) '&' ('not' (a2 '&' c2)) =
(('not' a2) 'or' ('not' b2)) '&' ('not' (a2 '&' c2))
by BVFUNC_1:14
.=
(('not' b2) 'or' ('not' a2)) '&' (('not' c2) 'or' ('not' a2))
by BVFUNC_1:14
.=
(b2 'imp' ('not' a2)) '&' (('not' c2) 'or' ('not' a2))
by BVFUNC_4:8
.=
(b2 'imp' ('not' a2)) '&' (c2 'imp' ('not' a2))
by BVFUNC_4:8
.=
(b2 'or' c2) 'imp' ('not' a2)
by Th75
;
then
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ((((b1 'or' c1) 'imp' (b2 'or' c2)) '&' ((b2 'or' c2) 'imp' ('not' a2))) '&' ((b1 'or' c1) 'imp' ('not' a2))) = I_el Y
by A6, Th12;
then A7:
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ((b1 'or' c1) 'imp' ('not' a2)) = I_el Y
by A1, BVFUNC_5:9;
( ((a1 'or' b1) 'or' c1) '&' ((b1 'or' c1) 'imp' ('not' a2)) = (a1 'or' (b1 'or' c1)) '&' ((b1 'or' c1) 'imp' ('not' a2)) & (a1 'or' (b1 'or' c1)) '&' ((b1 'or' c1) 'imp' ('not' a2)) '<' a1 'or' ('not' a2) )
by Th1, BVFUNC_1:8;
then A8:
(((a1 'or' b1) 'or' c1) '&' ((b1 'or' c1) 'imp' ('not' a2))) 'imp' (a1 'or' ('not' a2)) = I_el Y
by BVFUNC_1:16;
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ((a1 'or' b1) 'or' c1) = I_el Y
by Lm3, BVFUNC_1:16;
then
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (((a1 'or' b1) 'or' c1) '&' ((b1 'or' c1) 'imp' ('not' a2))) = I_el Y
by A7, th18;
then
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (a1 'or' ('not' a2)) = I_el Y
by A8, BVFUNC_5:9;
then
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (a2 'imp' a1) = I_el Y
by BVFUNC_4:8;
hence
((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' a2 'imp' a1
by BVFUNC_1:16; verum