set F = field (VertexAdjSymRel G);
now 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 Glet x,
y be
object ;
( 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 )
;
( [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;
verum end;
hence
VertexAdjSymRel G is connected
by RELAT_2:def 6, RELAT_2:def 14; verum