theorem Th84: :: GLIB_015:84

for F being non empty Graph-yielding Function
for x being Element of dom F holds (the_Edges_of (canGFDistinction F)) . x = [:{[(the_Edges_of F),x]},((the_Edges_of F) . x):]