theorem :: BVFUNC_6:116
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds (a '&' b) 'or' (c '&' d) '<' a 'or' c