let X be set ; :: thesis: for F being Field_Subset of X

for A, B being Subset of X st A in F & B in F holds

A \ B in F

let F be Field_Subset of X; :: thesis: for A, B being Subset of X st A in F & B in F holds

A \ B in F

let A, B be Subset of X; :: thesis: ( A in F & B in F implies A \ B in F )

assume A1: A in F ; :: thesis: ( not B in F or A \ B in F )

assume B in F ; :: thesis: A \ B in F

then B ` in F by Def1;

then A /\ (B `) in F by A1, FINSUB_1:def 2;

hence A \ B in F by SUBSET_1:13; :: thesis: verum

for A, B being Subset of X st A in F & B in F holds

A \ B in F

let F be Field_Subset of X; :: thesis: for A, B being Subset of X st A in F & B in F holds

A \ B in F

let A, B be Subset of X; :: thesis: ( A in F & B in F implies A \ B in F )

assume A1: A in F ; :: thesis: ( not B in F or A \ B in F )

assume B in F ; :: thesis: A \ B in F

then B ` in F by Def1;

then A /\ (B `) in F by A1, FINSUB_1:def 2;

hence A \ B in F by SUBSET_1:13; :: thesis: verum