let G be _Graph; :: thesis: ( ( for C being Component of G holds not C is _trivial ) implies VertexAdjSymRel G is total )
assume for C being Component of G holds not C is _trivial ; :: thesis: VertexAdjSymRel G is total
then A1: field (VertexDomRel G) = the_Vertices_of G by Th6;
dom (VertexAdjSymRel G) = (dom (VertexDomRel G)) \/ (dom ((VertexDomRel G) ~)) by XTUPLE_0:23
.= (dom (VertexDomRel G)) \/ (rng (VertexDomRel G)) by RELAT_1:20
.= the_Vertices_of G by A1, RELAT_1:def 6 ;
hence VertexAdjSymRel G is total by PARTFUN1:def 2; :: thesis: verum