theorem :: BVFUNC_6:148

for Y being non empty set
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))