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) "

thus ({} the carrier of G) " c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= ({} the carrier of G) "

proof

thus
{} c= ({} the carrier of G) "
; :: thesis: verum
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;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