theorem :: GFACIRC1:2

for x being Element of BOOLEAN holds
( buf1 . <*x*> = x & buf1 . <*x*> = and2 . <*x,x*> & buf1 . <*0*> = 0 & buf1 . <*1*> = 1 )