let G1 be addAdjVertexAll of G,v,V; :: thesis: not G1 is loopfull

per cases ( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G ) ;

suppose ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: not G1 is loopfull

hence not G1 is loopfull by Th14; :: thesis: verum

end;

suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: not G1 is loopfull

then G == G1 by GLIB_007:def 4;
hence not G1 is loopfull by Th4; :: thesis: verum

end;

end;