theorem Th123: :: GLIB_015:123

for F being non empty Graph-yielding Function
for z being Element of dom F ex S being GraphSum of F st
( S is Supergraph of F . z & S is GraphUnion of rng (canGFDistinction (F,z)) )