theorem tt: :: BVFUNC_6:21
for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a 'imp' b = I_el Y & c 'imp' d = I_el Y holds
(a '&' c) 'imp' (b '&' d) = I_el Y