:: deftheorem defines joins GRAPH_1:def 12 :
for G being Graph
for x, y being Element of the carrier of G
for v being set holds
( v joins x,y iff ( ( the Source of G . v = x & the Target of G . v = y ) or ( the Source of G . v = y & the Target of G . v = x ) ) );