let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN holds a 'or' b = ('not' a) 'imp' b
let a, b be Function of 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