theorem Th23: :: BVFUNC_6:125

for Y being non empty set
for a1, b1, c1, a2, b2, c2 being Function of Y,BOOLEAN holds ((((b1 'imp' b2) '&' (c1 'imp' c2)) '&' ((a1 'or' b1) 'or' c1)) '&' ('not' (a2 '&' b2))) '&' ('not' (a2 '&' c2)) '<' a2 'imp' a1