:: deftheorem Def4 defines UNION SETFAM_1:def 4 :
for SFX, SFY, b₃ being set holds
( b₃ = UNION (SFX,SFY) iff for Z being set holds
( Z in b₃ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) );