set H = the _trivial edgeless _Graph;
set v = the Vertex of the _trivial edgeless _Graph;
take G = the addEdge of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph, the_Edges_of the _trivial edgeless _Graph, the Vertex of the _trivial edgeless _Graph; :: thesis: ( G is _trivial & G is non-Dmulti & G is loopfull )
G is addLoops of the _trivial edgeless _Graph,{ the Vertex of the _trivial edgeless _Graph} by GLIB_012:27;
hence ( G is _trivial & G is non-Dmulti & G is loopfull ) ; :: thesis: verum