let G be addGroup; :: thesis: - ([#] the carrier of G) = the carrier of G
thus - ([#] the carrier of G) c= the carrier of G ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of G c= - ([#] the carrier of G)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of G or x in - ([#] the carrier of G) )
assume x in the carrier of G ; :: thesis: x in - ([#] the carrier of G)
then reconsider a = x as Element of G ;
- (- a) in [#] the carrier of G ;
hence x in - ([#] the carrier of G) ; :: thesis: verum