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