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)

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

then x in v + A by A4;

hence x in (v + A) \ (v + B) by A6, XBOOLE_0:def 5; :: thesis: verum

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 ; :: according to TARSKI:def 3 :: thesis: ( not x in v + (A \ B) or x in (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;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

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

w in A
by A5, XBOOLE_0:def 5;
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;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

then x in v + A by A4;

hence x in (v + A) \ (v + B) by A6, XBOOLE_0:def 5; :: thesis: verum