theorem :: BVFUNC_4:2

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st a '&' b '<' c holds
a '<' b 'imp' c