for x, y being Element of BOOLEAN holds or2 . <*x,y*> = 'not' (('not' x) '&' ('not' y)) by Lm1;