theorem Th16: :: PROB_1:16

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