let G be _Graph; :: thesis: for x, y being set holds
( x in G .AdjacentSet {y} iff y in G .AdjacentSet {x} )
let x, y be set ; :: thesis: ( x in G .AdjacentSet {y} iff y in G .AdjacentSet {x} )

hereby :: thesis: ( y in G .AdjacentSet {x} implies x in G .AdjacentSet {y} )

assume A1: x in G .AdjacentSet {y} ; :: thesis: y in G .AdjacentSet {x}
then reconsider xg = x as Vertex of G ;

now :: thesis: y in the_Vertices_of G

consider vy being Vertex of G such that
A2: vy in {y} and
vy,xg are_adjacent by A1, Th49;
assume A3: not y in the_Vertices_of G ; :: thesis: contradiction
vy = y by A2, TARSKI:def 1;
hence contradiction by A3; :: thesis: verum

end;

then reconsider yg = y as Vertex of G ;
A4: xg,yg are_adjacent by A1, Th51;
xg <> yg by A1, Th51;
hence y in G .AdjacentSet {x} by A4, Th51; :: thesis: verum

end;

assume A5: y in G .AdjacentSet {x} ; :: thesis: x in G .AdjacentSet {y}
then reconsider yg = y as Vertex of G ;

now :: thesis: x in the_Vertices_of G

consider vx being Vertex of G such that
A6: vx in {x} and
vx,yg are_adjacent by A5, Th49;
assume A7: not x in the_Vertices_of G ; :: thesis: contradiction
vx = x by A6, TARSKI:def 1;
hence contradiction by A7; :: thesis: verum

end;

then reconsider xg = x as Vertex of G ;
A8: xg,yg are_adjacent by A5, Th51;
xg <> yg by A5, Th51;
hence x in G .AdjacentSet {y} by A8, Th51; :: thesis: verum