set D2 = the carrier of (GroupCat UN);

now :: thesis: for x being object st x in { G where G is Element of the carrier of (GroupCat UN) : ex H being AbGroup st G = H } holds
x in the carrier of (GroupCat UN)

let x be object ; :: thesis: ( x in { G where G is Element of the carrier of (GroupCat UN) : ex H being AbGroup st G = H } implies x in the carrier of (GroupCat UN) )
assume x in { G where G is Element of the carrier of (GroupCat UN) : ex H being AbGroup st G = H } ; :: thesis: x in the carrier of (GroupCat UN)
then ex G being Element of the carrier of (GroupCat UN) st
( x = G & ex H being AbGroup st G = H ) ;
hence x in the carrier of (GroupCat UN) ; :: thesis: verum

end;

hence { G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H } is Subset of the carrier of (GroupCat UN) by TARSKI:def 3; :: thesis: verum