theorem :: BVFUNC_6:131

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN holds
( ((a '&' b) '&' c) '&' d '<' a & ((a '&' b) '&' c) '&' d '<' b ) by Lm3;