let G2 be inducedSubgraph of G, the_Vertices_of G,E; :: thesis: not G2 is loopfull

per cases ( E is Subset of (the_Edges_of G) or not E is Subset of (the_Edges_of G) ) ;

suppose E is Subset of (the_Edges_of G) ; :: thesis: not G2 is loopfull

hence not G2 is loopfull ; :: thesis: verum

end;

suppose E is not Subset of (the_Edges_of G) ; :: thesis: not G2 is loopfull

then not E c= G .edgesBetween (the_Vertices_of G) by GLIB_000:34;
then G == G2 by GLIB_000:def 37;
hence not G2 is loopfull by Th4; :: thesis: verum

end;

end;