let G be _Graph; :: thesis: ( G is _trivial & not G is loopless implies G is loopfull )
assume A2: ( G is _trivial & not G is loopless ) ; :: thesis: G is loopfull
let v be Vertex of G; :: according to GLIB_012:def 1 :: thesis: ex e being object st e Joins v,v,G
consider v0 being Vertex of G such that
A3: the_Vertices_of G = {v0} by A2, GLIB_000:22;
A4: v = v0 by A3, TARSKI:def 1;
consider v9 being object such that
A5: ex e being object st e Joins v9,v9,G by A2, GLIB_000:18;
consider e being object such that
A6: e Joins v9,v9,G by A5;
take e ; :: thesis: e Joins v,v,G
v9 in the_Vertices_of G by A6, GLIB_000:13;
then v9 = v0 by A3, TARSKI:def 1;
hence e Joins v,v,G by A4, A6; :: thesis: verum