let G be addGroup; :: thesis: for A, B being Subset of G holds - (A + B) = (- B) + (- A)
let A, B be Subset of G; :: thesis: - (A + B) = (- B) + (- A)
thus - (A + B) c= (- B) + (- A) :: according to XBOOLE_0:def 10 :: thesis: (- B) + (- A) c= - (A + B)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in - (A + B) or x in (- B) + (- A) )
assume x in - (A + B) ; :: thesis: x in (- B) + (- A)
then consider g being Element of G such that
A1: x = - g and
A2: g in A + B ;
consider g1, g2 being Element of G such that
A3: g = g1 + g2 and
A4: ( g1 in A & g2 in B ) by A2;
A5: ( - g1 in - A & - g2 in - B ) by A4;
x = (- g2) + (- g1) by A1, A3, Th16;
hence x in (- B) + (- A) by A5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- B) + (- A) or x in - (A + B) )
assume x in (- B) + (- A) ; :: thesis: x in - (A + B)
then consider g1, g2 being Element of G such that
A6: x = g1 + g2 and
A7: g1 in - B and
A8: g2 in - A ;
consider b being Element of G such that
A9: g2 = - b and
A10: b in A by A8;
consider a being Element of G such that
A11: g1 = - a and
A12: a in B by A7;
A13: b + a in A + B by A12, A10;
x = - (b + a) by A6, A11, A9, Th16;
hence x in - (A + B) by A13; :: thesis: verum