set F = field (VertexAdjSymRel G);

now :: thesis: for x, y being object st x in field (VertexAdjSymRel G) & y in field (VertexAdjSymRel G) & x <> y & not [x,y] in VertexAdjSymRel G holds
[y,x] in VertexAdjSymRel G

let x, y be object ; :: thesis: ( x in field (VertexAdjSymRel G) & y in field (VertexAdjSymRel G) & x <> y & not [x,y] in VertexAdjSymRel G implies [y,x] in VertexAdjSymRel G )
assume A1: ( x in field (VertexAdjSymRel G) & y in field (VertexAdjSymRel G) & x <> y ) ; :: thesis: ( [x,y] in VertexAdjSymRel G or [y,x] in VertexAdjSymRel G )
field (VertexAdjSymRel 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;
v,w are_adjacent by A1, CHORD:def 6;
hence ( [x,y] in VertexAdjSymRel G or [y,x] in VertexAdjSymRel G ) by Th33; :: thesis: verum

end;

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