:: deftheorem Def5 defines (/\) SETLIM_2:def 5 :
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) );