theorem :: BVFUNC_6:129

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' b '<' a by Lm1;