let X be set ; :: thesis: for S being Field_Subset of X
for A, B being set st A in S & B in S holds
A \ B in S
let S be Field_Subset of X; :: thesis: for A, B being set st A in S & B in S holds
A \ B in S
let A, B be set ; :: thesis: ( A in S & B in S implies A \ B in S )
assume A1: ( A in S & B in S ) ; :: thesis: A \ B in S
then A2: X \ B in S by Th19;
A /\ (X \ B) = (A /\ X) \ B by XBOOLE_1:49
.= A \ B by A1, XBOOLE_1:28 ;
hence A \ B in S by A1, A2, Th19; :: thesis: verum