now :: thesis: for x9 being Element of dom (canGFDistinction F) holds (canGFDistinction F) . x9 is plain
let x9 be Element of dom (canGFDistinction F); :: thesis: (canGFDistinction F) . x9 is plain
reconsider x = x9 as Element of dom F by Def25;
(canGFDistinction F) . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) by Def25;
hence (canGFDistinction F) . x9 is plain ; :: thesis: verum
end;
hence canGFDistinction F is plain by GLIBPRE0:def 2; :: thesis: verum