set F = field (VertexDomRel G);
now for x, y being object st x in field (VertexDomRel G) & y in field (VertexDomRel G) & x <> y & not [x,y] in VertexDomRel G holds
[y,x] in VertexDomRel Glet x,
y be
object ;
( x in field (VertexDomRel G) & y in field (VertexDomRel G) & x <> y & not [b1,b2] in VertexDomRel G implies [b2,b1] in VertexDomRel G )assume A1:
(
x in field (VertexDomRel G) &
y in field (VertexDomRel G) &
x <> y )
;
( [b1,b2] in VertexDomRel G or [b2,b1] in VertexDomRel G )
field (VertexDomRel G) c= (the_Vertices_of G) \/ (the_Vertices_of G)
by RELSET_1:8;
then reconsider v =
x,
w =
y as
Vertex of
G by A1;
consider e being
object such that A2:
e Joins v,
w,
G
by A1, CHORD:def 3, CHORD:def 6;
end;
hence
VertexDomRel G is connected
by RELAT_2:def 6, RELAT_2:def 14; verum