let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for A, B being Subset of V
for v being Element of V holds (v + A) \ (v + B) = v + (A \ B)
let A, B be Subset of V; :: thesis: for v being Element of V holds (v + A) \ (v + B) = v + (A \ B)
let v be Element of V; :: thesis: (v + A) \ (v + B) = v + (A \ B)
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: v + (A \ B) c= (v + A) \ (v + B)
let x be object ; :: thesis: ( x in (v + A) \ (v + B) implies x in v + (A \ B) )
assume A1: x in (v + A) \ (v + B) ; :: thesis: x in v + (A \ B)
then x in v + A by XBOOLE_0:def 5;
then consider w being Element of V such that
A2: x = v + w and
A3: w in A ;
not x in v + B by A1, XBOOLE_0:def 5;
then not w in B by A2;
then w in A \ B by A3, XBOOLE_0:def 5;
hence x in v + (A \ B) by A2; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in v + (A \ B) or x in (v + A) \ (v + B) )
assume x in v + (A \ B) ; :: thesis: x in (v + A) \ (v + B)
then consider w being Element of V such that
A4: x = v + w and
A5: w in A \ B ;
A6: not x in v + B
proof
assume x in v + B ; :: thesis: contradiction
then consider s being Element of V such that
A7: x = v + s and
A8: s in B ;
s = w by A4, A7, RLVECT_1:8;
hence contradiction by A5, A8, XBOOLE_0:def 5; :: thesis: verum
end;
w in A by A5, XBOOLE_0:def 5;
then x in v + A by A4;
hence x in (v + A) \ (v + B) by A6, XBOOLE_0:def 5; :: thesis: verum