for x, y, z being Element of BOOLEAN holds
( or3 . <*x,y,z*> = (x 'or' y) 'or' z & or3a . <*x,y,z*> = (('not' x) 'or' y) 'or' z & or3b . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' z & nand3 . <*x,y,z*> = (('not' x) 'or' ('not' y)) 'or' ('not' z) ) by FACIRC_1:def 7, Def15, Def16, Lm6;