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