:: deftheorem Def2 defines SemialgebraFamily MEASUR10:def 2 :
for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for b₃ being b₁ -element FinSequence holds
( b₃ is SemialgebraFamily of X iff for i being Nat st i in Seg n holds
b₃ . i is semialgebra_of_sets of X . i );