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