let Y be non empty set ; :: thesis:
let a1, b1, c1, a2, b2, c2 be Element of Funcs Y,BOOLEAN ; :: thesis:
A1: ((((b1 'or' c1) 'imp' (b2 'or' c2)) '&' ((b2 'or' c2) 'imp' ('not' a2))) '&' ((b1 'or' c1) 'imp' ('not' a2))) 'imp' ((b1 'or' c1) 'imp' ('not' a2)) = I_el Y by BVFUNC_6:39;
((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' c1 'imp' c2 by Lm4;
then A2: (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (c1 'imp' c2) = I_el Y by BVFUNC_1:19;
(b1 'imp' b2) '&' (c1 'imp' c2) '<' (b1 'or' c1) 'imp' (b2 'or' c2) by Th22;
then A3: ((b1 'imp' b2) '&' (c1 'imp' c2)) 'imp' ((b1 'or' c1) 'imp' (b2 'or' c2)) = I_el Y by BVFUNC_1:19;
((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' b1 'imp' b2 by Lm4;
then (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (b1 'imp' b2) = I_el Y by BVFUNC_1:19;
then (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ((b1 'imp' b2) '&' (c1 'imp' c2)) = I_el Y by A2, BVFUNC_6:18;
then A4: (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ((b1 'or' c1) 'imp' (b2 'or' c2)) = I_el Y by A3, BVFUNC_5:10;
((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' 'not' (a2 '&' c2) by Lm1;
then A5: (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ('not' (a2 '&' c2)) = I_el Y by BVFUNC_1:19;
((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' 'not' (a2 '&' b2) by Lm2;
then (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ('not' (a2 '&' b2)) = I_el Y by BVFUNC_1:19;
then (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (('not' (a2 '&' b2)) '&' ('not' (a2 '&' c2))) = I_el Y by A5, BVFUNC_6:18;
then A6: (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (((b1 'or' c1) 'imp' (b2 'or' c2)) '&' (('not' (a2 '&' b2)) '&' ('not' (a2 '&' c2)))) = I_el Y by A4, BVFUNC_6:18;
('not' (a2 '&' b2)) '&' ('not' (a2 '&' c2)) = (('not' a2) 'or' ('not' b2)) '&' ('not' (a2 '&' c2)) by BVFUNC_1:17
.= (('not' b2) 'or' ('not' a2)) '&' (('not' c2) 'or' ('not' a2)) by BVFUNC_1:17
.= (b2 'imp' ('not' a2)) '&' (('not' c2) 'or' ('not' a2)) by BVFUNC_4:8
.= (b2 'imp' ('not' a2)) '&' (c2 'imp' ('not' a2)) by BVFUNC_4:8
.= (b2 'or' c2) 'imp' ('not' a2) by BVFUNC_7:5 ;
then (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ((((b1 'or' c1) 'imp' (b2 'or' c2)) '&' ((b2 'or' c2) 'imp' ('not' a2))) '&' ((b1 'or' c1) 'imp' ('not' a2))) = I_el Y by A6, BVFUNC_7:12;
then A7: (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ((b1 'or' c1) 'imp' ('not' a2)) = I_el Y by A1, BVFUNC_5:10;
( ((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:11;
then A8: (((a1 'or' b1) 'or' c1) '&' ((b1 'or' c1) 'imp' ('not' a2))) 'imp' (a1 'or' ('not' a2)) = I_el Y by BVFUNC_1:19;
((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' (a1 'or' b1) 'or' c1 by Lm3;
then (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' ((a1 'or' b1) 'or' c1) = I_el Y by BVFUNC_1:19;
then (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (((a1 'or' b1) 'or' c1) '&' ((b1 'or' c1) 'imp' ('not' a2))) = I_el Y by A7, BVFUNC_6:18;
then (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (a1 'or' ('not' a2)) = I_el Y by A8, BVFUNC_5:10;
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:19; :: thesis: