for x, y being Element of BOOLEAN holds
( and2 . <*x,y*> = x '&' y & and2a . <*x,y*> = ('not' x) '&' y & nor2 . <*x,y*> = ('not' x) '&' ('not' y) ) by FACIRC_1:def 6, Def1, Lm3;