let Y be non empty set ; :: thesis:
let a1, a2, b1, b2, c1, c2 be Element of Funcs Y,BOOLEAN ; :: thesis:
let z be Element of Y; :: according to BVFUNC_1:def 15 :: thesis:
assume A1: ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) . z = TRUE ; :: thesis:
A2: ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) . z = ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) . z) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def 21
.= ((((a1 'imp' a2) '&' (b1 'imp' b2)) . z) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def 21
.= ((((a1 'imp' a2) . z) '&' ((b1 'imp' b2) . z)) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def 21
.= ((((('not' a1) 'or' a2) . z) '&' ((b1 'imp' b2) . z)) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_4:8
.= ((((('not' a1) 'or' a2) . z) '&' ((('not' b1) 'or' b2) . z)) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_4:8
.= ((((('not' a1) 'or' a2) . z) '&' ((('not' b1) 'or' b2) . z)) '&' ((('not' c1) 'or' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_4:8
.= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) 'or' b2) . z)) '&' ((('not' c1) 'or' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def 7
.= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) 'or' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def 7
.= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def 7
.= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 'or' b1) . z) 'or' (c1 . z)) by BVFUNC_1:def 7
.= ((((('not' a1) . z) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by BVFUNC_1:def 7
.= (((('not' (a1 . z)) 'or' (a2 . z)) '&' ((('not' b1) . z) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def 20
.= (((('not' (a1 . z)) 'or' (a2 . z)) '&' (('not' (b1 . z)) 'or' (b2 . z))) '&' ((('not' c1) . z) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def 20
.= (((('not' (a1 . z)) 'or' (a2 . z)) '&' (('not' (b1 . z)) 'or' (b2 . z))) '&' (('not' (c1 . z)) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def 20 ;

now

assume A3: ((a2 'or' b2) 'or' c2) . z <> TRUE ; :: thesis:
A4: ((a2 'or' b2) 'or' c2) . z = ((a2 'or' b2) . z) 'or' (c2 . z) by BVFUNC_1:def 7
.= ((a2 . z) 'or' (b2 . z)) 'or' (c2 . z) by BVFUNC_1:def 7 ;
A5: ( (a2 . z) 'or' (b2 . z) = TRUE or (a2 . z) 'or' (b2 . z) = FALSE ) by XBOOLEAN:def 3;
A6: ( c2 . z = TRUE or c2 . z = FALSE ) by XBOOLEAN:def 3;
( b2 . z = TRUE or b2 . z = FALSE ) by XBOOLEAN:def 3;
then A7: (((('not' (a1 . z)) 'or' (a2 . z)) '&' (('not' (b1 . z)) 'or' (b2 . z))) '&' (('not' (c1 . z)) 'or' (c2 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) = (((('not' a1) . z) '&' ('not' (b1 . z))) '&' ('not' (c1 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by A3, A4, A5, A6, MARGREL1:def 20
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' ('not' (c1 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def 20
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def 20
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 'or' b1) . z) 'or' (c1 . z)) by BVFUNC_1:def 7
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def 7
.= (((('not' a1) '&' ('not' b1)) . z) '&' (('not' c1) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def 21
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) . z) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def 21
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' ((a1 'or' b1) 'or' c1)) . z by MARGREL1:def 21 ;
((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' ((a1 'or' b1) 'or' c1) = (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' c1) by BVFUNC_1:15
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' ((('not' a1) '&' ('not' b1)) '&' (('not' c1) '&' c1)) by BVFUNC_1:7
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' ((('not' a1) '&' ('not' b1)) '&' (O_el Y)) by BVFUNC_4:5
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' (O_el Y) by BVFUNC_1:8
.= ((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1) by BVFUNC_1:12
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' b1) by BVFUNC_1:15
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' (((('not' a1) '&' ('not' c1)) '&' ('not' b1)) '&' b1) by BVFUNC_1:7
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' ((('not' a1) '&' ('not' c1)) '&' (('not' b1) '&' b1)) by BVFUNC_1:7
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' ((('not' a1) '&' ('not' c1)) '&' (O_el Y)) by BVFUNC_4:5
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' (O_el Y) by BVFUNC_1:8
.= ((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1 by BVFUNC_1:12
.= ((('not' b1) '&' ('not' c1)) '&' ('not' a1)) '&' a1 by BVFUNC_1:7
.= (('not' b1) '&' ('not' c1)) '&' (('not' a1) '&' a1) by BVFUNC_1:7
.= (('not' b1) '&' ('not' c1)) '&' (O_el Y) by BVFUNC_4:5
.= O_el Y by BVFUNC_1:8 ;
hence contradiction by A1, A2, A7, BVFUNC_1:def 13; :: thesis:

end;

hence ((a2 'or' b2) 'or' c2) . z = TRUE ; :: thesis: