:: deftheorem Def1 defines (/\) SETLIM_2:def 1 :
for X being set
for A1, A2, b₄ being SetSequence of X holds
( b₄ = A1 (/\) A2 iff for n being Nat holds b₄ . n = (A1 . n) /\ (A2 . n) );