let Y be non empty set ; :: thesis: for a, b, c, d being Function of Y,BOOLEAN holds a '&' ((b 'or' c) 'or' d) = ((a '&' b) 'or' (a '&' c)) 'or' (a '&' d)
let a, b, c, d be Function of Y,BOOLEAN; :: thesis: a '&' ((b 'or' c) 'or' d) = ((a '&' b) 'or' (a '&' c)) 'or' (a '&' d)
a '&' ((b 'or' c) 'or' d) = (a '&' (b 'or' c)) 'or' (a '&' d) by BVFUNC_1:12
.= ((a '&' b) 'or' (a '&' c)) 'or' (a '&' d) by BVFUNC_1:12 ;
hence a '&' ((b 'or' c) 'or' d) = ((a '&' b) 'or' (a '&' c)) 'or' (a '&' d) ; :: thesis: verum