let G be loopless _Graph; :: thesis: ( VertexAdjSymRel G is total implies for C being Component of G holds not C is _trivial )
assume VertexAdjSymRel G is total ; :: thesis: for C being Component of G holds not C is _trivial
then A1: dom (VertexAdjSymRel G) = the_Vertices_of G by PARTFUN1:def 2;
field (VertexDomRel G) = (field (VertexDomRel G)) \/ (field (VertexDomRel G))
.= (field (VertexDomRel G)) \/ (field ((VertexDomRel G) ~)) by RELAT_1:21
.= field (VertexAdjSymRel G) by RELAT_1:18
.= (dom (VertexAdjSymRel G)) \/ (rng (VertexAdjSymRel G)) by RELAT_1:def 6 ;
then A2: the_Vertices_of G c= field (VertexDomRel G) by A1, XBOOLE_1:7;
field (VertexDomRel G) c= (the_Vertices_of G) \/ (the_Vertices_of G) by RELSET_1:8;
hence for C being Component of G holds not C is _trivial by A2, Th5, XBOOLE_0:def 10; :: thesis: verum