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