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