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

A2: now

let A, B be set ; :: thesis: ( A in EX & B in EX implies A /\ B in EX )
assume A3: ( A in EX & B in EX ) ; :: thesis: A /\ B in EX
A4: ( ( A = {} or B = {} ) implies A /\ B = {} ) ;
( A = X & B = X implies A /\ B = X ) ;
hence A /\ B in EX by A3, A4, TARSKI:def 2; :: thesis: verum

end;

now

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

end;

hence {{} ,X} is Field_Subset of X by A2, Def1, FINSUB_1:def 2; :: thesis: verum