:: deftheorem Def6 defines (\/) SETLIM_2:def 6 :
for X being set
for A1 being SetSequence of X
for A being Subset of X
for b₄ being SetSequence of X holds
( b₄ = A (\/) A1 iff for n being Nat holds b₄ . n = A \/ (A1 . n) );