let X be set ; :: thesis: {{},X} is Field_Subset of X
( {} c= X & X in bool X ) by ZFMISC_1:def 1;
then reconsider EX = {{},X} as Subset-Family of X by Th2;
now :: thesis: for A being Subset of X st A in EX holds
A ` in EX
let A be Subset of X; :: thesis: ( A in EX implies A ` in EX )
A1: ( A = {} implies A ` = X ) ;
( A = X implies A ` = {} X ) by XBOOLE_1:37;
hence ( A in EX implies A ` in EX ) by A1, TARSKI:def 2; :: thesis: verum
end;
hence {{},X} is Field_Subset of X by Def1; :: thesis: verum