let A, B, X 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 that
A1: A in sigma_Field C and
A2: B in sigma_Field C ; :: thesis: A \ B in sigma_Field C
for x being object holds
( x in A \ B iff x in A /\ (X \ B) )

proof

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

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

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

end;

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

end;

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