:: deftheorem defines is_dependent_of BVFUNC_1:def 15 :
for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y holds
( a is_dependent_of PA iff for F being set st F in PA holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2 );