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