:: deftheorem Def1 defines '/\' BVFUNC_2:def 1 :
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b₃ being a_partition of Y holds
( b₃ = '/\' G iff for x being set holds
( x in b₃ iff ex h being Function ex F being Subset-Family of Y st
( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) ) );