:: deftheorem Def5 defines '\/' PARTIT1:def 5 :
for Y being non empty set
for PA, PB, b₄ being a_partition of Y holds
( b₄ = PA '\/' PB iff for d being set holds
( d in b₄ iff d is_min_depend PA,PB ) );