let G be _Graph; :: thesis: for u, v being Vertex of G holds
( u in G .AdjacentSet {v} iff ( u <> v & v,u are_adjacent ) )
let u, v be Vertex of G; :: thesis: ( u in G .AdjacentSet {v} iff ( u <> v & v,u are_adjacent ) )

hereby :: thesis: ( u <> v & v,u are_adjacent implies u in G .AdjacentSet {v} )

assume A1: u in G .AdjacentSet {v} ; :: thesis: ( u <> v & v,u are_adjacent )
then consider x being Vertex of G such that
A2: ( x in {v} & u,x are_adjacent ) by Th50;
x = v by A2, TARSKI:def 1;
hence ( u <> v & v,u are_adjacent ) by A1, A2, Th50; :: thesis: verum

end;

assume A3: ( u <> v & v,u are_adjacent ) ; :: thesis: u in G .AdjacentSet {v}
then ( not u in {v} & v in {v} ) by TARSKI:def 1;
hence u in G .AdjacentSet {v} by A3; :: thesis: verum