theorem FieldGen1: :: SRINGS_3:21

for X being set
for P being semialgebra_of_sets of X holds P c= Field_generated_by P