:: deftheorem defines union TARSKI:def 4 :
for X, b₂ being set holds
( b₂ = union X iff for x being object holds
( x in b₂ iff ex Y being set st
( x in Y & Y in X ) ) );