set D2 = the carrier of (AbGroupCat UN);

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

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

end;

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