let G2 be Subgraph of G; :: thesis: G2 is _trivial
card (the_Vertices_of G) = 1 by Def19;
then consider v being object such that
A1: the_Vertices_of G = {v} by CARD_2:42;
the_Vertices_of G2 = {v} by A1, ZFMISC_1:33;
then card (the_Vertices_of G2) = 1 by CARD_1:30;
hence G2 is _trivial ; :: thesis: verum