now :: thesis: for x1, x2 being Element of dom (canGFDistinction F) st x1 <> x2 holds
(the_Vertices_of (canGFDistinction F)) . x1 misses (the_Vertices_of (canGFDistinction F)) . x2
let x1, x2 be Element of dom (canGFDistinction F); :: thesis: ( x1 <> x2 implies (the_Vertices_of (canGFDistinction F)) . x1 misses (the_Vertices_of (canGFDistinction F)) . x2 )
( x1 in dom (canGFDistinction F) & x2 in dom (canGFDistinction F) ) ;
then A1: ( x1 in dom F & x2 in dom F ) by Def25;
assume A2: x1 <> x2 ; :: thesis: (the_Vertices_of (canGFDistinction F)) . x1 misses (the_Vertices_of (canGFDistinction F)) . x2
A3: (the_Vertices_of (canGFDistinction F)) . x1 = [:{[(the_Vertices_of F),x1]},((the_Vertices_of F) . x1):] by A1, Th83
.= rng (renameElementsDistinctlyFunc ((the_Vertices_of F),x1)) by Th80 ;
(the_Vertices_of (canGFDistinction F)) . x2 = [:{[(the_Vertices_of F),x2]},((the_Vertices_of F) . x2):] by A1, Th83
.= rng (renameElementsDistinctlyFunc ((the_Vertices_of F),x2)) by Th80 ;
hence (the_Vertices_of (canGFDistinction F)) . x1 misses (the_Vertices_of (canGFDistinction F)) . x2 by A2, A3, Th82; :: thesis: verum
end;
hence canGFDistinction F is vertex-disjoint by Th70; :: thesis: canGFDistinction F is edge-disjoint
now :: thesis: for x1, x2 being Element of dom (canGFDistinction F) st x1 <> x2 holds
(the_Edges_of (canGFDistinction F)) . x1 misses (the_Edges_of (canGFDistinction F)) . x2
let x1, x2 be Element of dom (canGFDistinction F); :: thesis: ( x1 <> x2 implies (the_Edges_of (canGFDistinction F)) . x1 misses (the_Edges_of (canGFDistinction F)) . x2 )
( x1 in dom (canGFDistinction F) & x2 in dom (canGFDistinction F) ) ;
then A4: ( x1 in dom F & x2 in dom F ) by Def25;
assume A5: x1 <> x2 ; :: thesis: (the_Edges_of (canGFDistinction F)) . x1 misses (the_Edges_of (canGFDistinction F)) . x2
A6: (the_Edges_of (canGFDistinction F)) . x1 = [:{[(the_Edges_of F),x1]},((the_Edges_of F) . x1):] by A4, Th84
.= rng (renameElementsDistinctlyFunc ((the_Edges_of F),x1)) by Th80 ;
(the_Edges_of (canGFDistinction F)) . x2 = [:{[(the_Edges_of F),x2]},((the_Edges_of F) . x2):] by A4, Th84
.= rng (renameElementsDistinctlyFunc ((the_Edges_of F),x2)) by Th80 ;
hence (the_Edges_of (canGFDistinction F)) . x1 misses (the_Edges_of (canGFDistinction F)) . x2 by A5, A6, Th82; :: thesis: verum
end;
hence canGFDistinction F is edge-disjoint by Th71; :: thesis: verum