take G9 = the GraphUnion of rng (canGFDistinction F); :: thesis: ex G9 being GraphUnion of rng (canGFDistinction F) st G9 is G9 -Disomorphic
G9 is G9 -Disomorphic by GLIB_010:53;
hence ex G9 being GraphUnion of rng (canGFDistinction F) st G9 is G9 -Disomorphic ; :: thesis: verum