theorem :: BVFUNC_1:27

for Y being non empty set
for a being Function of Y,BOOLEAN
for x being Element of Y holds a . x <= (B_SUP a) . x