let Y be non empty set ; :: thesis: for a being Element of Funcs Y,BOOLEAN holds a = ('not' a) 'imp' a
let a be Element of Funcs Y,BOOLEAN ; :: thesis: a = ('not' a) 'imp' a
a 'imp' (('not' a) 'imp' a) = I_el Y by Th22;
then A1: a '<' ('not' a) 'imp' a by BVFUNC_1:19;
(('not' a) 'imp' a) 'imp' a = I_el Y by BVFUNC_5:12;
then ('not' a) 'imp' a '<' a by BVFUNC_1:19;
hence a = ('not' a) 'imp' a by A1, BVFUNC_1:18; :: thesis: verum