:: deftheorem Def2 defines " MEASURE6:def 3 :
for X, Y being set
for f being Function of X,Y
for b₄ being Function of (bool Y),(bool X) holds
( b₄ = " f iff for y being Subset of Y holds b₄ . y = f " y );