let x be Element of BOOLEAN ; :: thesis: ( inv1 . <*x*> = 'not' x & inv1 . <*x*> = nand2 . <*x,x*> & inv1 . <*0*> = 1 & inv1 . <*1*> = 0 )
thus inv1 . <*x*> = 'not' x by Def1; :: thesis: ( inv1 . <*x*> = nand2 . <*x,x*> & inv1 . <*0*> = 1 & inv1 . <*1*> = 0 )
thus inv1 . <*x*> = 'not' (x '&' x) by Def1
.= nand2 . <*x,x*> by TWOSCOMP:def 4 ; :: thesis: ( inv1 . <*0*> = 1 & inv1 . <*1*> = 0 )
thus inv1 . <*0*> = 'not' FALSE by Def1
.= 1 ; :: thesis: inv1 . <*1*> = 0
thus inv1 . <*1*> = 'not' TRUE by Def1
.= 0 ; :: thesis: verum