let G be Group; :: 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