let x, y, z be Element of BOOLEAN ; :: thesis: or3 . <*x,y,z*> = 'not' ((('not' x) '&' ('not' y)) '&' ('not' z))
thus or3 . <*x,y,z*> = (x 'or' y) 'or' z by FACIRC_1:def 7
.= 'not' ((('not' x) '&' ('not' y)) '&' ('not' z)) ; :: thesis: verum