:: deftheorem Defsigmaring defines sigmaring SRINGS_3:def 5 :
for X being set
for S being Subset-Family of X
for b₃ being SigmaRing of X holds
( b₃ = sigmaring S iff ( S c= b₃ & ( for Z being set st S c= Z & Z is SigmaRing of X holds
b₃ c= Z ) ) );