let G be _Graph; ( G is _trivial & not G is loopless implies G is loopfull )
assume A2:
( G is _trivial & not G is loopless )
; G is loopfull
let v be Vertex of G; GLIB_012:def 1 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
; 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; verum