theorem :: SRINGS_2:4

for X being set
for F being SigmaField of X holds F is semiring_of_sets of X ;