set T = Trivial-addLoopStr ;
set D2 = the carrier of (AbGroupCat UN);
set D1 = { G where G is Element of the carrier of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ;
Trivial-addLoopStr in the carrier of (AbGroupCat UN) by Th36;
then Trivial-addLoopStr in { G where G is Element of the carrier of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } ;
then reconsider D1 = { G where G is Element of the carrier of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H } as non empty set ;

now :: thesis: for x being set st x in D1 holds
x in the carrier of (AbGroupCat UN)

let x be set ; :: thesis: ( x in D1 implies x in the carrier of (AbGroupCat UN) )
assume x in D1 ; :: 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 not MidOpGroupObjects UN is empty ; :: thesis: verum