let x be Element of BOOLEAN ; :: thesis: ( buf1 . <*x*> = x & buf1 . <*x*> = and2 . <*x,x*> & buf1 . <*0*> = 0 & buf1 . <*1*> = 1 )
thus buf1 . <*x*> = x by Def2; :: thesis: ( buf1 . <*x*> = and2 . <*x,x*> & buf1 . <*0*> = 0 & buf1 . <*1*> = 1 )
thus buf1 . <*x*> = x '&' x by Def2
.= and2 . <*x,x*> by FACIRC_1:def 6 ; :: thesis: ( buf1 . <*0*> = 0 & buf1 . <*1*> = 1 )
thus buf1 . <*0*> = FALSE by Def2
.= 0 ; :: thesis: buf1 . <*1*> = 1
thus buf1 . <*1*> = TRUE by Def2
.= 1 ; :: thesis: verum