for X being set
for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds P c= Ring_generated_by P