let X be set ; :: thesis: for F being Field_Subset of X ex A being Subset of X st A in F
let F be Field_Subset of X; :: thesis: ex A being Subset of X st A in F
consider A being Element of F;
( A in F & F c= bool X ) ;
hence ex A being Subset of X st A in F ; :: thesis: verum