let X, A, B be set ; :: thesis: for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A \ B in sigma_Field C
let C be C_Measure of X; :: thesis: ( A in sigma_Field C & B in sigma_Field C implies A \ B in sigma_Field C )
assume A1: ( A in sigma_Field C & B in sigma_Field C ) ; :: thesis: A \ B in sigma_Field C
for x being set holds
( x in A \ B iff x in A /\ (X \ B) )

proof

let x be set ; :: thesis: ( x in A \ B iff x in A /\ (X \ B) )

hereby :: thesis: ( x in A /\ (X \ B) implies x in A \ B )

assume x in A \ B ; :: thesis: x in A /\ (X \ B)
then ( x in A & not x in B ) by XBOOLE_0:def 5;
then ( x in A & x in X \ B ) by A1, XBOOLE_0:def 5;
hence x in A /\ (X \ B) by XBOOLE_0:def 4; :: thesis: verum

end;

assume x in A /\ (X \ B) ; :: thesis: x in A \ B
then ( x in A & x in X \ B ) by XBOOLE_0:def 4;
then ( x in A & x in X & not x in B ) by XBOOLE_0:def 5;
hence x in A \ B by XBOOLE_0:def 5; :: thesis: verum

end;

then A2: A \ B = A /\ (X \ B) by TARSKI:2;
X \ B in sigma_Field C by A1, Th16;
hence A \ B in sigma_Field C by A1, A2, Th18; :: thesis: verum