let Y be non empty set ; :: thesis: for a, b, c being Element of Funcs (Y,BOOLEAN) st a 'imp' c = I_el Y & b 'imp' c = I_el Y holds
(a '&' b) 'imp' c = I_el Y
let a, b, c be Element of Funcs (Y,BOOLEAN); :: thesis: ( a 'imp' c = I_el Y & b 'imp' c = I_el Y implies (a '&' b) 'imp' c = I_el Y )
( a 'imp' c = I_el Y & b 'imp' c = I_el Y implies (a '&' b) 'imp' (c '&' c) = I_el Y ) by BVFUNC_6:21;
hence ( a 'imp' c = I_el Y & b 'imp' c = I_el Y implies (a '&' b) 'imp' c = I_el Y ) ; :: thesis: verum