:: deftheorem Def3 defines are_adjacent CHORD:def 3 :
for G being _Graph
for a, b being Vertex of G holds
( a,b are_adjacent iff ex e being object st e Joins a,b,G );