let Y be non empty set ; :: thesis: for a, b being Element of Funcs (Y,BOOLEAN) holds a 'or' b = ('not' a) 'imp' b
let a, b be Element of Funcs (Y,BOOLEAN); :: thesis: a 'or' b = ('not' a) 'imp' b
thus ('not' a) 'imp' b = ('not' ('not' a)) 'or' b by BVFUNC_4:8
.= a 'or' b ; :: thesis: verum