theorem Th38: :: GLUNIR00:38

for G being _Graph st ( for C being Component of G holds not C is _trivial ) holds
VertexAdjSymRel G is total