theorem th18: :: BVFUNC_6:18

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN st c 'imp' a = I_el Y & c 'imp' b = I_el Y holds
c 'imp' (a '&' b) = I_el Y