for x being Element of BOOLEAN holds
( inv1 . <*x*> = 'not' x & inv1 . <*x*> = nand2 . <*x,x*> & inv1 . <*0*> = 1 & inv1 . <*1*> = 0 )