now :: thesis: for C being Component of G holds not C is _trivial

let C be Component of G; :: thesis: not C is _trivial
set v = the Vertex of C;
the_Vertices_of C c= the_Vertices_of G ;
then ( the Vertex of C in the_Vertices_of G & G is Component of G ) by GLIB_002:30, TARSKI:def 3;
then C == G by GLIB_002:34;
hence not C is _trivial by GLIB_000:89; :: thesis: verum

end;

hence VertexAdjSymRel G is total by Th38; :: thesis: verum