let G be addGroup; :: thesis: - ({} the carrier of G) = {}
thus - ({} the carrier of G) c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= - ({} the carrier of G)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in - ({} the carrier of G) or x in {} )
assume x in - ({} the carrier of G) ; :: thesis: x in {}
then ex a being Element of G st
( x = - a & a in {} the carrier of G ) ;
hence x in {} ; :: thesis: verum
end;
thus {} c= - ({} the carrier of G) ; :: thesis: verum