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