for Y being set
for f being real-valued Function holds (0 (#) f) | Y is bounded