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;

A1: now

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

end;

now

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

end;

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