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;

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

( 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 that 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;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

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