let G2 be Subgraph of G; :: thesis: G2 is trivial
card (the_Vertices_of G) = 1 by Def21;
then consider v being set such that
A1: the_Vertices_of G = {v} by CARD_2:60;
the_Vertices_of G2 = {v} by A1, ZFMISC_1:39;
then card (the_Vertices_of G2) = 1 by CARD_1:50;
hence G2 is trivial by Def21; :: thesis: verum