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} )

then reconsider yg = y 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

( 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 A5:
y in G .AdjacentSet {x}
; :: thesis: 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 ;

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;then reconsider xg = x as Vertex of G ;

now :: thesis: y in the_Vertices_of G

then reconsider yg = y as Vertex 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;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

A4: xg,yg are_adjacent by A1, Th51;

xg <> yg by A1, Th51;

hence y in G .AdjacentSet {x} by A4, Th51; :: thesis: verum

then reconsider yg = y as Vertex of G ;

now :: thesis: x in the_Vertices_of G

then reconsider xg = x as Vertex 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;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

A8: xg,yg are_adjacent by A5, Th51;

xg <> yg by A5, Th51;

hence x in G .AdjacentSet {y} by A8, Th51; :: thesis: verum