theorem Th4: :: BVFUNC25:50

for Y being non empty set
for a being Function of Y,BOOLEAN holds (O_el Y) 'nand' a = I_el Y