let G2 be inducedSubgraph of G,V; :: thesis: G2 is loopfull

per cases ( V is non empty Subset of (the_Vertices_of G) or not V is non empty Subset of (the_Vertices_of G) ) ;

suppose A1: V is non empty Subset of (the_Vertices_of G) ; :: thesis: G2 is loopfull

let v be Vertex of G2; :: according to GLIB_012:def 1 :: thesis: ex e being object st e Joins v,v,G2
v in the_Vertices_of G2 ;
then reconsider v0 = v as Vertex of G ;
consider e being object such that
A2: e Joins v0,v0,G by Def1;
take e ; :: thesis: e Joins v,v,G2
the_Vertices_of G2 = V by A1, GLIB_000:def 37;
then e in G .edgesBetween V by A2, GLIB_000:32;
then ( e in the_Edges_of G2 & e is set & v is set ) by A1, GLIB_000:def 37;
hence e Joins v,v,G2 by A2, GLIB_000:73; :: thesis: verum

end;

suppose V is not non empty Subset of (the_Vertices_of G) ; :: thesis: G2 is loopfull

then G2 == G by GLIB_000:def 37;
hence G2 is loopfull by Th4; :: thesis: verum

end;

end;