for X being set
for F being Field_Subset of X holds F is semialgebra_of_sets of X by Def1, PROB_1:5;