for x being set st x in GroupObjects UN holds
x is strict AddGroup by Th43;
hence GroupObjects UN is Group_DOMAIN-like by Def22; :: thesis: verum