let G be _Graph; :: thesis: for v, w being Vertex of G holds
( v,w are_adjacent iff w in v .allNeighbors() )
let v, w be Vertex of G; :: thesis: ( v,w are_adjacent iff w in v .allNeighbors() )

hereby :: thesis: ( w in v .allNeighbors() implies v,w are_adjacent )

assume v,w are_adjacent ; :: thesis: w in v .allNeighbors()
then ex e being object st e Joins v,w,G by CHORD:def 3;
hence w in v .allNeighbors() by GLIB_000:71; :: thesis: verum

end;

assume w in v .allNeighbors() ; :: thesis: v,w are_adjacent
then ex e being object st e Joins v,w,G by GLIB_000:71;
hence v,w are_adjacent by CHORD:def 3; :: thesis: verum