set D = {Trivial-addLoopStr };
take {Trivial-addLoopStr } ; :: thesis: ( {Trivial-addLoopStr } is Group_DOMAIN-like & not {Trivial-addLoopStr } is empty )
for x being set 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 ) by Def22; :: thesis: verum