theorem Th5: :: GLUNIR00:5

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