let Y be non empty set ; :: thesis: for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) '<' (('not' (a1 '&' b1)) '&' ('not' (a1 '&' c1))) '&' ('not' (b1 '&' c1))
let a1, b1, c1, a2, b2, c2 be Function of Y,BOOLEAN; :: thesis: (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) '<' (('not' (a1 '&' b1)) '&' ('not' (a1 '&' c1))) '&' ('not' (b1 '&' c1))
A1: (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2)))) 'imp' ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) = I_el Y by Th38;
A2: (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2))) 'imp' ('not' (a1 '&' c1)) = I_el Y by Th25;
((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) 'imp' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2))) = I_el Y by Th38;
then (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2)))) 'imp' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2))) = I_el Y by A1, BVFUNC_5:9;
then A3: (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2)))) 'imp' ('not' (a1 '&' c1)) = I_el Y by A2, BVFUNC_5:9;
A4: (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) 'imp' ('not' (a1 '&' b1)) = I_el Y by Th25;
( (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2)))) 'imp' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2))) = I_el Y & (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2))) 'imp' ('not' (b1 '&' c1)) = I_el Y ) by Th25, Th38;
then A5: (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2)))) 'imp' ('not' (b1 '&' c1)) = I_el Y by BVFUNC_5:9;
((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) 'imp' (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) = I_el Y by Th38;
then (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2)))) 'imp' (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) = I_el Y by A1, BVFUNC_5:9;
then (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2)))) 'imp' ('not' (a1 '&' b1)) = I_el Y by A4, BVFUNC_5:9;
then (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2)))) 'imp' (('not' (a1 '&' b1)) '&' ('not' (a1 '&' c1))) = I_el Y by A3, th18;
then A6: (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2)))) 'imp' ((('not' (a1 '&' b1)) '&' ('not' (a1 '&' c1))) '&' ('not' (b1 '&' c1))) = I_el Y by A5, th18;
(((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) = ((((((a1 'imp' a2) '&' (a1 'imp' a2)) '&' ((b1 'imp' b2) '&' (b1 'imp' b2))) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2))
.= (((((((a1 'imp' a2) '&' (a1 'imp' a2)) '&' (b1 'imp' b2)) '&' (b1 'imp' b2)) '&' ((c1 'imp' c2) '&' (c1 'imp' c2))) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) by BVFUNC_1:4
.= (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (a1 'imp' a2)) '&' (b1 'imp' b2)) '&' ((c1 'imp' c2) '&' (c1 'imp' c2))) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) by BVFUNC_1:4
.= ((((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (a1 'imp' a2)) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) by BVFUNC_1:4
.= (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (a1 'imp' a2)) '&' ((b1 'imp' b2) '&' (c1 'imp' c2))) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) by BVFUNC_1:4
.= (((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((b1 'imp' b2) '&' (c1 'imp' c2))) '&' (a1 'imp' a2)) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) by BVFUNC_1:4
.= ((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((b1 'imp' b2) '&' (c1 'imp' c2))) '&' ((a1 'imp' a2) '&' (c1 'imp' c2))) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) by BVFUNC_1:4
.= ((((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((b1 'imp' b2) '&' (c1 'imp' c2))) '&' ((a1 'imp' a2) '&' (c1 'imp' c2))) '&' ('not' (a2 '&' c2))) '&' ('not' (a2 '&' b2))) '&' ('not' (b2 '&' c2)) by BVFUNC_1:4
.= (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((b1 'imp' b2) '&' (c1 'imp' c2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' ('not' (a2 '&' b2))) '&' ('not' (b2 '&' c2)) by BVFUNC_1:4
.= (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ((b1 'imp' b2) '&' (c1 'imp' c2))) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' ('not' (b2 '&' c2)) by BVFUNC_1:4
.= (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' ((b1 'imp' b2) '&' (c1 'imp' c2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' ('not' (b2 '&' c2)) by BVFUNC_1:4
.= (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' ((b1 'imp' b2) '&' (c1 'imp' c2))) '&' ('not' (b2 '&' c2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2))) by BVFUNC_1:4
.= ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2)))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2))) by BVFUNC_1:4
.= ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) '&' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2)))) '&' (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2))) by BVFUNC_1:4 ;
hence (((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2))) '&' ('not' (b2 '&' c2)) '<' (('not' (a1 '&' b1)) '&' ('not' (a1 '&' c1))) '&' ('not' (b1 '&' c1)) by A6, BVFUNC_1:16; :: thesis: verum