let G be addGroup; :: thesis: for A, B being Subset of G holds
( A c= B iff - A c= - B )
let A, B be Subset of G; :: thesis: ( A c= B iff - A c= - B )
( - (- A) = A & - (- B) = B ) ;
hence ( A c= B iff - A c= - B ) by Lm1; :: thesis: verum