theorem :: BVFUNC_1:23

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