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 set ; :: 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 consider a being Element of G such that
x = a " and
A1: a in {} the carrier of G ;
thus x in {} by A1; :: thesis: verum

end;

thus {} c= ({} the carrier of G) " by XBOOLE_1:2; :: thesis: verum