:: deftheorem Def1 defines union HALLMAR1:def 1 :
for F being set
for A being FinSequence of bool F
for J, b₄ being set holds
( b₄ = union (A,J) iff for x being object holds
( x in b₄ iff ex j being set st
( j in J & j in dom A & x in A . j ) ) );