:: deftheorem defines vertices GRAPH_5:def 1 :
for G being Graph
for e being Element of the carrier' of G holds vertices e = {( the Source of G . e),( the Target of G . e)};