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:
then reconsider xg = x as Vertex of G ;
now :: thesis:
consider vy being Vertex of G such that
A2: vy in {y} and
vy,xg are_adjacent by ;
assume A3: not y in the_Vertices_of G ; :: thesis: contradiction
vy = y by ;
hence contradiction by A3; :: thesis: verum
end;
then reconsider yg = y as Vertex of G ;
A4: xg,yg are_adjacent by ;
xg <> yg by ;
hence y in G .AdjacentSet {x} by ; :: thesis: verum
end;
assume A5: y in G .AdjacentSet {x} ; :: thesis:
then reconsider yg = y as Vertex of G ;
now :: thesis:
consider vx being Vertex of G such that
A6: vx in {x} and
vx,yg are_adjacent by ;
assume A7: not x in the_Vertices_of G ; :: thesis: contradiction
vx = x by ;
hence contradiction by A7; :: thesis: verum
end;
then reconsider xg = x as Vertex of G ;
A8: xg,yg are_adjacent by ;
xg <> yg by ;
hence x in G .AdjacentSet {y} by ; :: thesis: verum