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

for A, B being set st A in F & B in F holds

(A \ B) \/ B in F

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

(A \ B) \/ B in F

let A, B be set ; :: thesis: ( A in F & B in F implies (A \ B) \/ B in F )

A \/ B = (A \ B) \/ B by XBOOLE_1:39;

hence ( A in F & B in F implies (A \ B) \/ B in F ) by Th3; :: thesis: verum

for A, B being set st A in F & B in F holds

(A \ B) \/ B in F

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

(A \ B) \/ B in F

let A, B be set ; :: thesis: ( A in F & B in F implies (A \ B) \/ B in F )

A \/ B = (A \ B) \/ B by XBOOLE_1:39;

hence ( A in F & B in F implies (A \ B) \/ B in F ) by Th3; :: thesis: verum