:: deftheorem defines are_incident GRAPH_1:def 13 :
for G being Graph
for x, y being Element of the carrier of G holds
( x,y are_incident iff ex v being set st
( v in the carrier' of G & v joins x,y ) );