for X, Y being set st Y is SigmaField of X holds
Y is Field_Subset of X