:: deftheorem Def1 defines Partial_Intersection PROB_3:def 1 :
for X being set
for A1, b₃ being SetSequence of X holds
( b₃ = Partial_Intersection A1 iff ( b₃ . 0 = A1 . 0 & ( for n being Nat holds b₃ . (n + 1) = (b₃ . n) /\ (A1 . (n + 1)) ) ) );