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

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