:: deftheorem Def3 defines '\/' BVFUNC_2:def 3 :
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b₃ being a_partition of Y holds
( ( G <> {} implies ( b₃ = '\/' G iff for x being set holds
( x in b₃ iff x is_upper_min_depend_of G ) ) ) & ( not G <> {} implies ( b₃ = '\/' G iff b₃ = %I Y ) ) );