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 ) )
A1: v in {v} by TARSKI:def 1;

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

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

end;

assume that
A5: u <> v and
A6: v,u are_adjacent ; :: thesis: u in G .AdjacentSet {v}
not u in {v} by A5, TARSKI:def 1;
hence u in G .AdjacentSet {v} by A6, A1; :: thesis: verum