:: deftheorem Def5 defines ClassicalSemiringFamily SRINGS_4:def 6 :
for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for b₃ being b₁ -element FinSequence holds
( b₃ is ClassicalSemiringFamily of X iff for i being Nat st i in Seg n holds
b₃ . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i) );