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