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

per cases ( V \ (the_Vertices_of G) <> {} or V \ (the_Vertices_of G) = {} ) ;

suppose V \ (the_Vertices_of G) <> {} ; :: thesis: not G1 is loopfull

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

end;

suppose V \ (the_Vertices_of G) = {} ; :: thesis: not G1 is loopfull

then G == G1 by GLIB_006:78, XBOOLE_1:37;
hence not G1 is loopfull by Th4; :: thesis: verum

end;

end;