let X be set ; :: thesis: {{},X} is Field_Subset of X
( {} c= X & X in bool X ) by XBOOLE_1:2, ZFMISC_1:def 1;
then reconsider EX = {{},X} as Subset-Family of X by Th4;

now

let A be Subset of X; :: thesis: ( A in EX implies A ` in EX )
A2: ( A = {} implies A ` = X ) ;
( A = X implies A ` = {} X ) by XBOOLE_1:37;
hence ( A in EX implies A ` in EX ) by A2, TARSKI:def 2; :: thesis: verum

end;

hence {{},X} is Field_Subset of X by Def1; :: thesis: verum