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;

( {} 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

hence
{{},X} is Field_Subset of X
by Def1; :: thesis: verumA ` 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;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