now :: thesis: for y1, y2 being Element of dom (canGFDistinction (F,z)) st y1 <> y2 holds
( (the_Vertices_of (canGFDistinction (F,z))) . y1 misses (the_Vertices_of (canGFDistinction (F,z))) . y2 & (the_Edges_of (canGFDistinction (F,z))) . y1 misses (the_Edges_of (canGFDistinction (F,z))) . y2 )
set G = canGFDistinction F;
set H = canGFDistinction (F,z);
let y1, y2 be Element of dom (canGFDistinction (F,z)); :: thesis: ( y1 <> y2 implies ( (the_Vertices_of (canGFDistinction (F,z))) . b1 misses (the_Vertices_of (canGFDistinction (F,z))) . b2 & (the_Edges_of (canGFDistinction (F,z))) . b1 misses (the_Edges_of (canGFDistinction (F,z))) . b2 ) )
( y1 in dom (canGFDistinction (F,z)) & y2 in dom (canGFDistinction (F,z)) ) ;
then A1: ( y1 in dom (canGFDistinction F) & y2 in dom (canGFDistinction F) ) by FUNCT_7:30;
then reconsider x1 = y1, x2 = y2 as Element of dom F by Def25;
assume A2: y1 <> y2 ; :: thesis: ( (the_Vertices_of (canGFDistinction (F,z))) . b1 misses (the_Vertices_of (canGFDistinction (F,z))) . b2 & (the_Edges_of (canGFDistinction (F,z))) . b1 misses (the_Edges_of (canGFDistinction (F,z))) . b2 )
per cases ( ( x1 <> z & x2 <> z ) or x1 = z or x2 = z ) ;
suppose A3: ( x1 <> z & x2 <> z ) ; :: thesis: ( (the_Vertices_of (canGFDistinction (F,z))) . b1 misses (the_Vertices_of (canGFDistinction (F,z))) . b2 & (the_Edges_of (canGFDistinction (F,z))) . b1 misses (the_Edges_of (canGFDistinction (F,z))) . b2 )
A4: ( (the_Vertices_of (canGFDistinction F)) . x1 misses (the_Vertices_of (canGFDistinction F)) . x2 & (the_Edges_of (canGFDistinction F)) . x1 misses (the_Edges_of (canGFDistinction F)) . x2 ) by A1, A2, Th73;
then (the_Vertices_of (canGFDistinction (F,z))) . x1 misses (the_Vertices_of (canGFDistinction F)) . x2 by A3, Th98;
hence (the_Vertices_of (canGFDistinction (F,z))) . y1 misses (the_Vertices_of (canGFDistinction (F,z))) . y2 by A3, Th98; :: thesis: (the_Edges_of (canGFDistinction (F,z))) . y1 misses (the_Edges_of (canGFDistinction (F,z))) . y2
(the_Edges_of (canGFDistinction (F,z))) . x1 misses (the_Edges_of (canGFDistinction F)) . x2 by A3, A4, Th101;
hence (the_Edges_of (canGFDistinction (F,z))) . y1 misses (the_Edges_of (canGFDistinction (F,z))) . y2 by A3, Th101; :: thesis: verum
end;
suppose A5: x1 = z ; :: thesis: ( (the_Vertices_of (canGFDistinction (F,z))) . b1 misses (the_Vertices_of (canGFDistinction (F,z))) . b2 & (the_Edges_of (canGFDistinction (F,z))) . b1 misses (the_Edges_of (canGFDistinction (F,z))) . b2 )
then A6: (the_Vertices_of (canGFDistinction (F,z))) . x1 = (the_Vertices_of F) . x1 by Th97
.= the_Vertices_of (F . x1) by Def8 ;
(the_Vertices_of (canGFDistinction (F,z))) . x2 = (the_Vertices_of (canGFDistinction F)) . x2 by A2, A5, Th98
.= [:{[(the_Vertices_of F),x2]},((the_Vertices_of F) . x2):] by Th83 ;
hence (the_Vertices_of (canGFDistinction (F,z))) . y1 misses (the_Vertices_of (canGFDistinction (F,z))) . y2 by A6, Lm4; :: thesis: (the_Edges_of (canGFDistinction (F,z))) . y1 misses (the_Edges_of (canGFDistinction (F,z))) . y2
A7: (the_Edges_of (canGFDistinction (F,z))) . x1 = (the_Edges_of F) . x1 by A5, Th100
.= the_Edges_of (F . x1) by Def9 ;
(the_Edges_of (canGFDistinction (F,z))) . x2 = (the_Edges_of (canGFDistinction F)) . x2 by A2, A5, Th101
.= [:{[(the_Edges_of F),x2]},((the_Edges_of F) . x2):] by Th84 ;
hence (the_Edges_of (canGFDistinction (F,z))) . y1 misses (the_Edges_of (canGFDistinction (F,z))) . y2 by A7, Lm5; :: thesis: verum
end;
suppose A8: x2 = z ; :: thesis: ( (the_Vertices_of (canGFDistinction (F,z))) . b1 misses (the_Vertices_of (canGFDistinction (F,z))) . b2 & (the_Edges_of (canGFDistinction (F,z))) . b1 misses (the_Edges_of (canGFDistinction (F,z))) . b2 )
then A9: (the_Vertices_of (canGFDistinction (F,z))) . x2 = (the_Vertices_of F) . x2 by Th97
.= the_Vertices_of (F . x2) by Def8 ;
(the_Vertices_of (canGFDistinction (F,z))) . x1 = (the_Vertices_of (canGFDistinction F)) . x1 by A2, A8, Th98
.= [:{[(the_Vertices_of F),x1]},((the_Vertices_of F) . x1):] by Th83 ;
hence (the_Vertices_of (canGFDistinction (F,z))) . y1 misses (the_Vertices_of (canGFDistinction (F,z))) . y2 by A9, Lm4; :: thesis: (the_Edges_of (canGFDistinction (F,z))) . y1 misses (the_Edges_of (canGFDistinction (F,z))) . y2
A10: (the_Edges_of (canGFDistinction (F,z))) . x2 = (the_Edges_of F) . x2 by A8, Th100
.= the_Edges_of (F . x2) by Def9 ;
(the_Edges_of (canGFDistinction (F,z))) . x1 = (the_Edges_of (canGFDistinction F)) . x1 by A2, A8, Th101
.= [:{[(the_Edges_of F),x1]},((the_Edges_of F) . x1):] by Th84 ;
hence (the_Edges_of (canGFDistinction (F,z))) . y1 misses (the_Edges_of (canGFDistinction (F,z))) . y2 by A10, Lm5; :: thesis: verum
end;
end;
end;
hence ( canGFDistinction (F,z) is vertex-disjoint & canGFDistinction (F,z) is edge-disjoint ) by Th73; :: thesis: verum