let F1, F2 be non empty Graph-yielding Function; :: thesis: ( F1,F2 are_Disomorphic implies canGFDistinction F1, canGFDistinction F2 are_Disomorphic )
assume A1: F1,F2 are_Disomorphic ; :: thesis: canGFDistinction F1, canGFDistinction F2 are_Disomorphic
canGFDistinction F1,F1 are_Disomorphic by Th87;
then A2: canGFDistinction F1,F2 are_Disomorphic by A1, Th40;
F2, canGFDistinction F2 are_Disomorphic by Th87;
hence canGFDistinction F1, canGFDistinction F2 are_Disomorphic by A2, Th40; :: thesis: verum