let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN holds (O_el Y) 'nand' a = I_el Y
let a be Function of Y,BOOLEAN; :: thesis: (O_el Y) 'nand' a = I_el Y
( (O_el Y) 'nand' a = 'not' ((O_el Y) '&' a) & (O_el Y) '&' a = O_el Y ) by th1, BVFUNC_1:5;
hence (O_el Y) 'nand' a = I_el Y by BVFUNC_1:2; :: thesis: verum