set D = {Trivial-addLoopStr};
take {Trivial-addLoopStr} ; :: thesis: ( {Trivial-addLoopStr} is Group_DOMAIN-like & not {Trivial-addLoopStr} is empty )
for x being object st x in {Trivial-addLoopStr} holds
x is strict AddGroup by TARSKI:def 1;
hence ( {Trivial-addLoopStr} is Group_DOMAIN-like & not {Trivial-addLoopStr} is empty ) ; :: thesis: verum