let G be addGroup; :: thesis: for A being Subset of G
for a being Element of G holds
( a in - A iff - a in A )
let A be Subset of G; :: thesis: for a being Element of G holds
( a in - A iff - a in A )
let a be Element of G; :: thesis: ( a in - A iff - a in A )
( - (- a) = a & - (- A) = A ) ;
hence ( a in - A iff - a in A ) ; :: thesis: verum