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