theorem :: SRINGS_4:16

for X being set
for S being cup-closed cap-closed with_empty_element Subset-Family of X holds semidiff S is semiring_of_sets of X ;