let G be non _trivial connected _Graph; :: thesis: field (VertexDomRel G) = the_Vertices_of G
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 field (VertexDomRel G) = the_Vertices_of G by Th6; :: thesis: verum