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