:: deftheorem Def4 defines cap-closed-yielding SRINGS_4:def 5 :
for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being SemiringFamily of X holds
( S is cap-closed-yielding iff for i being Nat st i in Seg n holds
S . i is cap-closed );