let G be loopless _Graph; :: thesis: ( field (VertexDomRel G) = the_Vertices_of G implies for C being Component of G holds not C is _trivial )
assume A1: field (VertexDomRel G) = the_Vertices_of G ; :: thesis: for C being Component of G holds not C is _trivial
let C be Component of G; :: thesis: not C is _trivial
assume C is _trivial ; :: thesis: contradiction
then consider v being Vertex of C such that
A2: the_Vertices_of C = {v} by GLIB_000:22;
A3: v in the_Vertices_of G by A2, ZFMISC_1:31;
reconsider v0 = v as Vertex of G by A2, ZFMISC_1:31;
the_Vertices_of G = (dom (VertexDomRel G)) \/ (rng (VertexDomRel G)) by A1, RELAT_1:def 6;
per cases then ( v in dom (VertexDomRel G) or v in rng (VertexDomRel G) ) by A3, XBOOLE_0:def 3;
suppose v in dom (VertexDomRel G) ; :: thesis: contradiction
then consider w being object such that
A4: [v,w] in VertexDomRel G by XTUPLE_0:def 12;
consider e being object such that
A5: e DJoins v,w,G by A4, Th1;
e Joins v,w,G by A5, GLIB_000:16;
then w in G .reachableFrom v0 by GLIB_002:9, GLIB_002:10;
then w in the_Vertices_of C by GLIB_002:33;
then w = v by A2, TARSKI:def 1;
hence contradiction by A5, GLIB_009:17; :: thesis: verum
end;
suppose v in rng (VertexDomRel G) ; :: thesis: contradiction
then consider w being object such that
A6: [w,v] in VertexDomRel G by XTUPLE_0:def 13;
consider e being object such that
A7: e DJoins w,v,G by A6, Th1;
e Joins v,w,G by A7, GLIB_000:16;
then w in G .reachableFrom v0 by GLIB_002:9, GLIB_002:10;
then w in the_Vertices_of C by GLIB_002:33;
then w = v by A2, TARSKI:def 1;
hence contradiction by A7, GLIB_009:17; :: thesis: verum
end;
end;