let Y be non empty set ; :: thesis: for a1, a2, b1, b2 being Function of Y,BOOLEAN holds (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))
let a1, a2, b1, b2 be Function of Y,BOOLEAN; :: thesis: (((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2)) '<' (((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))
let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not ((((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z = TRUE or ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE )
A1: ((((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z = ((((('not' a1) 'or' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z by BVFUNC_4:8
.= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z by BVFUNC_4:8
.= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) '&' (a1 'or' a2)) . z) '&' (('not' (b1 '&' b2)) . z) by MARGREL1:def 20
.= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) . z) '&' ((a1 'or' a2) . z)) '&' (('not' (b1 '&' b2)) . z) by MARGREL1:def 20
.= ((((('not' a1) 'or' b1) '&' (('not' a2) 'or' b2)) . z) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:14
.= ((((('not' a1) 'or' b1) . z) '&' ((('not' a2) 'or' b2) . z)) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by MARGREL1:def 20
.= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) 'or' b2) . z)) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:def 4
.= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 'or' a2) . z)) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:def 4
.= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) 'or' ('not' b2)) . z) by BVFUNC_1:def 4
.= ((((('not' a1) . z) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) . z) 'or' (('not' b2) . z)) by BVFUNC_1:def 4
.= (((('not' (a1 . z)) 'or' (b1 . z)) '&' ((('not' a2) . z) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) . z) 'or' (('not' b2) . z)) by MARGREL1:def 19
.= (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' ((('not' b1) . z) 'or' (('not' b2) . z)) by MARGREL1:def 19
.= (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' (('not' b2) . z)) by MARGREL1:def 19
.= (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) by MARGREL1:def 19 ;
assume A2: ((((a1 'imp' b1) '&' (a2 'imp' b2)) '&' (a1 'or' a2)) '&' ('not' (b1 '&' b2))) . z = TRUE ; :: thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE

now :: thesis: ( ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z <> TRUE implies ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE )

A3: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = ((((('not' b1) 'or' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z by BVFUNC_4:8
.= ((((('not' b1) 'or' a1) '&' (('not' b2) 'or' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z by BVFUNC_4:8
.= ((((('not' b1) 'or' a1) '&' (('not' b2) 'or' a2)) '&' (b1 'or' b2)) . z) '&' (('not' (a1 '&' a2)) . z) by MARGREL1:def 20
.= ((((('not' b1) 'or' a1) '&' (('not' b2) 'or' a2)) . z) '&' ((b1 'or' b2) . z)) '&' (('not' (a1 '&' a2)) . z) by MARGREL1:def 20
.= ((((('not' b1) 'or' a1) . z) '&' ((('not' b2) 'or' a2) . z)) '&' ((b1 'or' b2) . z)) '&' (('not' (a1 '&' a2)) . z) by MARGREL1:def 20
.= ((((('not' b1) 'or' a1) . z) '&' ((('not' b2) 'or' a2) . z)) '&' ((b1 'or' b2) . z)) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:14
.= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) 'or' a2) . z)) '&' ((b1 'or' b2) . z)) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:def 4
.= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 'or' b2) . z)) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:def 4
.= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z))) '&' ((('not' a1) 'or' ('not' a2)) . z) by BVFUNC_1:def 4
.= ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z))) '&' ((('not' a1) . z) 'or' (('not' a2) . z)) by BVFUNC_1:def 4 ;
assume ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z <> TRUE ; :: thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE
then A4: ((((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z))) '&' ((('not' a1) . z) 'or' (('not' a2) . z)) = FALSE by A3, XBOOLEAN:def 3;

now :: thesis: ( ( (((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z)) = FALSE & ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ) or ( (('not' a1) . z) 'or' (('not' a2) . z) = FALSE & ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ) )

per cases ( (((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z)) = FALSE or (('not' a1) . z) 'or' (('not' a2) . z) = FALSE ) by A4, MARGREL1:12;

case A5: (((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z))) '&' ((b1 . z) 'or' (b2 . z)) = FALSE ; :: thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE

now :: thesis: ( ( ((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z)) = FALSE & ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ) or ( (b1 . z) 'or' (b2 . z) = FALSE & ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ) )

per cases ( ((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z)) = FALSE or (b1 . z) 'or' (b2 . z) = FALSE ) by A5, MARGREL1:12;

case A6: ((('not' b1) . z) 'or' (a1 . z)) '&' ((('not' b2) . z) 'or' (a2 . z)) = FALSE ; :: thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE

now :: thesis: ( ( (('not' b1) . z) 'or' (a1 . z) = FALSE & ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ) or ( (('not' b2) . z) 'or' (a2 . z) = FALSE & ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ) )

per cases ( (('not' b1) . z) 'or' (a1 . z) = FALSE or (('not' b2) . z) 'or' (a2 . z) = FALSE ) by A6, MARGREL1:12;

case A7: (('not' b1) . z) 'or' (a1 . z) = FALSE ; :: thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE

A8: ( a1 . z = TRUE or a1 . z = FALSE ) by XBOOLEAN:def 3;
then 'not' (b1 . z) = FALSE by A7, MARGREL1:def 19;
then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = (((a2 . z) '&' ('not' (a2 . z))) 'or' ((a2 . z) '&' (b2 . z))) '&' ('not' (b2 . z)) by A7, A8, XBOOLEAN:8
.= (FALSE 'or' ((a2 . z) '&' (b2 . z))) '&' ('not' (b2 . z)) by XBOOLEAN:138
.= ((a2 . z) '&' (b2 . z)) '&' ('not' (b2 . z))
.= (a2 . z) '&' ((b2 . z) '&' ('not' (b2 . z)))
.= FALSE '&' (a2 . z) by XBOOLEAN:138
.= FALSE ;
hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; :: thesis: verum

end;

case A9: (('not' b2) . z) 'or' (a2 . z) = FALSE ; :: thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE

A10: ( a2 . z = TRUE or a2 . z = FALSE ) by XBOOLEAN:def 3;
then 'not' (b2 . z) = FALSE by A9, MARGREL1:def 19;
then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = (((a1 . z) '&' ('not' (a1 . z))) 'or' ((a1 . z) '&' (b1 . z))) '&' ('not' (b1 . z)) by A9, A10, XBOOLEAN:8
.= (FALSE 'or' ((a1 . z) '&' (b1 . z))) '&' ('not' (b1 . z)) by XBOOLEAN:138
.= ((a1 . z) '&' (b1 . z)) '&' ('not' (b1 . z))
.= (a1 . z) '&' ((b1 . z) '&' ('not' (b1 . z)))
.= FALSE '&' (a1 . z) by XBOOLEAN:138
.= FALSE ;
hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; :: thesis: verum

end;

end;

end;

hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; :: thesis: verum

end;

case A11: (b1 . z) 'or' (b2 . z) = FALSE ; :: thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE

reconsider a2z = a2 . z as boolean object ;
reconsider a1z = a1 . z as boolean object ;
( b1 . z = TRUE or b1 . z = FALSE ) by XBOOLEAN:def 3;
then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = ('not' (a1 . z)) '&' (('not' (a2 . z)) '&' ((a1 . z) 'or' (a2 . z))) by A11
.= ('not' (a1 . z)) '&' ((('not' (a2 . z)) '&' (a1 . z)) 'or' (('not' a2z) '&' a2z)) by XBOOLEAN:8
.= ('not' (a1 . z)) '&' ((('not' (a2 . z)) '&' (a1 . z)) 'or' FALSE) by XBOOLEAN:138
.= ('not' (a1 . z)) '&' ((a1 . z) '&' ('not' (a2 . z)))
.= (('not' a1z) '&' a1z) '&' ('not' (a2 . z))
.= FALSE '&' ('not' (a2 . z)) by XBOOLEAN:138
.= FALSE ;
hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; :: thesis: verum

end;

end;

end;

hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; :: thesis: verum

end;

case A12: (('not' a1) . z) 'or' (('not' a2) . z) = FALSE ; :: thesis: ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE

( ('not' a2) . z = TRUE or ('not' a2) . z = FALSE ) by XBOOLEAN:def 3;
then ( 'not' (a1 . z) = FALSE & 'not' (a2 . z) = FALSE ) by A12, MARGREL1:def 19;
then (((('not' (a1 . z)) 'or' (b1 . z)) '&' (('not' (a2 . z)) 'or' (b2 . z))) '&' ((a1 . z) 'or' (a2 . z))) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))) = (b1 . z) '&' ((b2 . z) '&' (('not' (b1 . z)) 'or' ('not' (b2 . z))))
.= (b1 . z) '&' (((b2 . z) '&' ('not' (b1 . z))) 'or' ((b2 . z) '&' ('not' (b2 . z)))) by XBOOLEAN:8
.= (b1 . z) '&' (((b2 . z) '&' ('not' (b1 . z))) 'or' FALSE) by XBOOLEAN:138
.= (b1 . z) '&' (('not' (b1 . z)) '&' (b2 . z))
.= ((b1 . z) '&' ('not' (b1 . z))) '&' (b2 . z)
.= FALSE '&' (b2 . z) by XBOOLEAN:138
.= FALSE ;
hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE by A2, A1; :: thesis: verum

end;

end;

end;

hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; :: thesis: verum

end;

hence ((((b1 'imp' a1) '&' (b2 'imp' a2)) '&' (b1 'or' b2)) '&' ('not' (a1 '&' a2))) . z = TRUE ; :: thesis: verum