theorem Th6: :: GLUNIR00:6

for G being _Graph st ( for C being Component of G holds not C is _trivial ) holds
field (VertexDomRel G) = the_Vertices_of G