let Y be non empty set ; :: thesis: for a1, b1, c1, a2, b2, c2 being Element of Funcs 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 Element of Funcs 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)) '&' (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:7
.= (((((((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:7
.= ((((((((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:7
.= (((((((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:7
.= (((((((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:7
.= ((((((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:7
.= ((((((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:7
.= (((((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:7
.= (((((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:7
.= (((((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:7
.= (((((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:7
.= ((((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:7
.= ((((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:7 ;
A2: (((((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 BVFUNC_6:39;
A3: ((((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 BVFUNC_6:39;
A4: ((((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 BVFUNC_6:39;
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' (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) = I_el Y by A2, A3, BVFUNC_5:10;
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' (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2))) = I_el Y by A2, A4, BVFUNC_5:10;
A7: (((((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 by BVFUNC_6:39;
A8: (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' ('not' (a2 '&' b2))) 'imp' ('not' (a1 '&' b1)) = I_el Y by Th26;
A9: (((a1 'imp' a2) '&' (c1 'imp' c2)) '&' ('not' (a2 '&' c2))) 'imp' ('not' (a1 '&' c1)) = I_el Y by Th26;
A10: (((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ('not' (b2 '&' c2))) 'imp' ('not' (b1 '&' c1)) = I_el Y by Th26;
A11: (((((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 A5, A8, BVFUNC_5:10;
A12: (((((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 A6, A9, BVFUNC_5:10;
A13: (((((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 A7, A10, BVFUNC_5:10;
(((((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 A11, A12, BVFUNC_6:18;
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))) '&' ('not' (b1 '&' c1))) = I_el Y by A13, BVFUNC_6:18;
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 A1, BVFUNC_1:19; :: thesis: verum