let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN holds a 'imp' b = ('not' b) 'imp' ('not' a)
let a, b be Function of Y,BOOLEAN; :: thesis: a 'imp' b = ('not' b) 'imp' ('not' a)
(a 'imp' b) 'imp' (('not' b) 'imp' ('not' a)) = I_el Y by BVFUNC_5:32;
then A1: a 'imp' b '<' ('not' b) 'imp' ('not' a) by BVFUNC_1:16;
(('not' b) 'imp' ('not' a)) 'imp' (a 'imp' b) = I_el Y by BVFUNC_5:31;
then ('not' b) 'imp' ('not' a) '<' a 'imp' b by BVFUNC_1:16;
hence a 'imp' b = ('not' b) 'imp' ('not' a) by A1, BVFUNC_1:15; :: thesis: verum