let Y be non empty set ; :: thesis: 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 'or' b) = I_el Y
let a, b, c be Function of 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 Th73
.= I_el Y by A1 ;
hence c 'imp' (a 'or' b) = I_el Y ; :: thesis: verum