let G be _Graph; :: thesis: ( G is loopfull implies not G is loopless )
assume G is loopfull ; :: thesis: not G is loopless
then consider e being object such that
A1: e Joins the Vertex of G, the Vertex of G,G ;
thus not G is loopless by A1, GLIB_000:18; :: thesis: verum