let Y be non empty set ; for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds ((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) '<' ((a2 'imp' a1) '&' (b2 'imp' b1)) '&' (c2 'imp' c1)
let a1, b1, c1, a2, b2, c2 be Function of Y,BOOLEAN; ((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) '<' ((a2 'imp' a1) '&' (b2 'imp' b1)) '&' (c2 'imp' c1)
A1:
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) = I_el Y
by Lm9;
( (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2))) = I_el Y & (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (b2 '&' a2))) '&' ('not' (b2 '&' c2))) = I_el Y )
by Lm7, Lm8;
then
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' ((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2))) '&' (((((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (b2 '&' a2))) '&' ('not' (b2 '&' c2)))) = I_el Y
by th18;
then A2:
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2))) '&' (((((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (b2 '&' c2)))) '&' (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)))) = I_el Y
by A1, th18;
A3:
(((((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (b2 '&' c2))) 'imp' (b2 'imp' b1) = I_el Y
by Th23, BVFUNC_1:16;
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2))) '&' (((((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (b2 '&' c2)))) '&' (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)))) 'imp' (((((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (b2 '&' c2))) = I_el Y
by Lm2, BVFUNC_1:16;
then
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (b2 '&' c2))) = I_el Y
by A2, BVFUNC_5:9;
then A4:
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (b2 'imp' b1) = I_el Y
by A3, BVFUNC_5:9;
(((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) 'imp' (a2 'imp' a1) = I_el Y
by Th23, BVFUNC_1:16;
then
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (a2 'imp' a1) = I_el Y
by A1, BVFUNC_5:9;
then A5:
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' ((a2 'imp' a1) '&' (b2 'imp' b1)) = I_el Y
by A4, th18;
((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' c1) 'or' b1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2)) '<' c2 'imp' c1
by Th23;
then
((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2)) '<' c2 'imp' c1
by BVFUNC_1:8;
then A6:
(((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2))) 'imp' (c2 'imp' c1) = I_el Y
by BVFUNC_1:16;
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2))) '&' (((((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (b2 '&' c2)))) '&' (((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)))) 'imp' (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2))) = I_el Y
by Lm2, BVFUNC_1:16;
then
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (c2 '&' a2))) '&' ('not' (c2 '&' b2))) = I_el Y
by A2, BVFUNC_5:9;
then
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (c2 'imp' c1) = I_el Y
by A6, BVFUNC_5:9;
then
(((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))) 'imp' (((a2 'imp' a1) '&' (b2 'imp' b1)) '&' (c2 'imp' c1)) = I_el Y
by A5, th18;
hence
((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) '<' ((a2 'imp' a1) '&' (b2 'imp' b1)) '&' (c2 'imp' c1)
by BVFUNC_1:16; verum