theorem :: GLUNIR00:37

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