theorem :: BVFUNC_6:128

for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of 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))