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 object ; :: 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

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 object ; :: 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