let X be set ; :: thesis: for F being Field_Subset of X holds {} in F
let F be Field_Subset of X; :: thesis: {} in F
consider A being Subset of X such that
A1: A in F by SUBSET_1:4;
A misses A ` by XBOOLE_1:79;
then A2: A /\ (A `) = {} by XBOOLE_0:def 7;
A ` in F by A1, Def1;
hence {} in F by A1, A2, FINSUB_1:def 2; :: thesis: verum