theorem Th15: :: BVFUNC_1:16

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a 'imp' b = I_el Y iff a '<' b )