let G2 be loopfull _Graph; :: thesis: for G1 being Supergraph of G2 st the_Vertices_of G1 = the_Vertices_of G2 holds
G1 is loopfull
let G1 be Supergraph of G2; :: thesis: ( the_Vertices_of G1 = the_Vertices_of G2 implies G1 is loopfull )
assume A1: the_Vertices_of G1 = the_Vertices_of G2 ; :: thesis: G1 is loopfull
let v be Vertex of G1; :: according to GLIB_012:def 1 :: thesis: ex e being object st e Joins v,v,G1
consider e being object such that
A2: e Joins v,v,G2 by A1, Def1;
take e ; :: thesis: e Joins v,v,G1
thus e Joins v,v,G1 by A2, GLIB_006:70; :: thesis: verum