set F = field (VertexDomRel G);

now :: thesis: 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 G

let x, y be object ; :: thesis: ( x in field (VertexDomRel G) & y in field (VertexDomRel G) & x <> y & not [b₁,b₂] in VertexDomRel G implies [b₂,b₁] in VertexDomRel G )
assume A1: ( x in field (VertexDomRel G) & y in field (VertexDomRel G) & x <> y ) ; :: thesis: ( [b₁,b₂] in VertexDomRel G or [b₂,b₁] 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;

per cases ( e DJoins v,w,G or e DJoins w,v,G ) by A2, GLIB_000:16;

suppose e DJoins v,w,G ; :: thesis: ( [b₁,b₂] in VertexDomRel G or [b₂,b₁] in VertexDomRel G )

hence ( [x,y] in VertexDomRel G or [y,x] in VertexDomRel G ) by Th1; :: thesis: verum

end;

suppose e DJoins w,v,G ; :: thesis: ( [b₁,b₂] in VertexDomRel G or [b₂,b₁] in VertexDomRel G )

hence ( [x,y] in VertexDomRel G or [y,x] in VertexDomRel G ) by Th1; :: thesis: verum

end;

end;

end;

hence VertexDomRel G is connected by RELAT_2:def 6, RELAT_2:def 14; :: thesis: verum