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