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