:: deftheorem Def1 defines dom GRAPH_1:def 1 :
for C being MultiGraphStruct
for f being Edge of C holds
( ( not C is void & not C is empty implies dom f = the Source of C . f ) & ( ( C is void or C is empty ) implies dom f = the Vertex of C ) );