let IT be inducedSubgraph of G,{v},E; :: thesis: IT is trivial
the_Vertices_of IT = {v} by Def39;
then card (the_Vertices_of IT) = 1 by CARD_1:30;
hence IT is trivial by Def21; :: thesis: verum