for X being set
for S being Field_Subset of X holds
( {} in S & X in S ) by PROB_1:4, PROB_1:5;