set G = the addLoops of the Dcomplete _Graph;
take the addLoops of the Dcomplete _Graph ; :: thesis: ( the addLoops of the Dcomplete _Graph is loopfull & the addLoops of the Dcomplete _Graph is Dcomplete )
thus ( the addLoops of the Dcomplete _Graph is loopfull & the addLoops of the Dcomplete _Graph is Dcomplete ) ; :: thesis: verum