let Y be non empty set ; :: thesis: for a1, a2, b1, b2, c1, c2 being Function of Y,BOOLEAN holds (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1) '<' (a2 'or' b2) 'or' c2
let a1, a2, b1, b2, c1, c2 be Function of Y,BOOLEAN; :: thesis: (((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1) '<' (a2 'or' b2) 'or' c2
let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) . z = TRUE or ((a2 'or' b2) 'or' c2) . z = TRUE )
A1: ((((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 20
.= ((((a1 'imp' a2) '&' (b1 'imp' b2)) . z) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def 20
.= ((((a1 'imp' a2) . z) '&' ((b1 'imp' b2) . z)) '&' ((c1 'imp' c2) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def 20
.= ((((('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 4
.= ((((('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 4
.= ((((('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 4
.= ((((('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 4
.= ((((('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 4
.= (((('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 19
.= (((('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 19
.= (((('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 19 ;
assume A2: ((((a1 'imp' a2) '&' (b1 'imp' b2)) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) . z = TRUE ; :: thesis: ((a2 'or' b2) 'or' c2) . z = TRUE

now :: thesis: not ((a2 'or' b2) 'or' c2) . z <> TRUE

A3: ( b2 . z = TRUE or b2 . z = FALSE ) by XBOOLEAN:def 3;
A4: ( c2 . z = TRUE or c2 . z = FALSE ) by XBOOLEAN:def 3;
A5: ((('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:12
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1)) 'or' ((('not' a1) '&' ('not' b1)) '&' (('not' c1) '&' c1)) by BVFUNC_1:4
.= (((('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:5
.= ((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' (a1 'or' b1) by BVFUNC_1:9
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' b1) by BVFUNC_1:12
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' (((('not' a1) '&' ('not' c1)) '&' ('not' b1)) '&' b1) by BVFUNC_1:4
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1) 'or' ((('not' a1) '&' ('not' c1)) '&' (('not' b1) '&' b1)) by BVFUNC_1:4
.= (((('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:5
.= ((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' a1 by BVFUNC_1:9
.= ((('not' b1) '&' ('not' c1)) '&' ('not' a1)) '&' a1 by BVFUNC_1:4
.= (('not' b1) '&' ('not' c1)) '&' (('not' a1) '&' a1) by BVFUNC_1:4
.= (('not' b1) '&' ('not' c1)) '&' (O_el Y) by BVFUNC_4:5
.= O_el Y by BVFUNC_1:5 ;
A6: ( (a2 . z) 'or' (b2 . z) = TRUE or (a2 . z) 'or' (b2 . z) = FALSE ) by XBOOLEAN:def 3;
A7: ((a2 'or' b2) 'or' c2) . z = ((a2 'or' b2) . z) 'or' (c2 . z) by BVFUNC_1:def 4
.= ((a2 . z) 'or' (b2 . z)) 'or' (c2 . z) by BVFUNC_1:def 4 ;
assume ((a2 'or' b2) 'or' c2) . z <> TRUE ; :: thesis: contradiction
then (((('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 A7, A6, A4, A3, MARGREL1:def 19
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' ('not' (c1 . z))) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def 19
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 . z) 'or' (b1 . z)) 'or' (c1 . z)) by MARGREL1:def 19
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 'or' b1) . z) 'or' (c1 . z)) by BVFUNC_1:def 4
.= (((('not' a1) . z) '&' (('not' b1) . z)) '&' (('not' c1) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by BVFUNC_1:def 4
.= (((('not' a1) '&' ('not' b1)) . z) '&' (('not' c1) . z)) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def 20
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) . z) '&' (((a1 'or' b1) 'or' c1) . z) by MARGREL1:def 20
.= (((('not' a1) '&' ('not' b1)) '&' ('not' c1)) '&' ((a1 'or' b1) 'or' c1)) . z by MARGREL1:def 20 ;
hence contradiction by A2, A1, A5, BVFUNC_1:def 10; :: thesis: verum

end;

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