theorem :: BVFUNC_1:25

for Y being non empty set
for a being Function of Y,BOOLEAN
for d being constant Function of Y,BOOLEAN holds
( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )