let F be non empty Graph-yielding Function; :: thesis: ( ( F is vertex-disjoint & F is edge-disjoint ) iff for x1, x2 being Element of dom F st x1 <> x2 holds
( (the_Vertices_of F) . x1 misses (the_Vertices_of F) . x2 & (the_Edges_of F) . x1 misses (the_Edges_of F) . x2 ) )
thus ( F is vertex-disjoint & F is edge-disjoint implies for x1, x2 being Element of dom F st x1 <> x2 holds
( (the_Vertices_of F) . x1 misses (the_Vertices_of F) . x2 & (the_Edges_of F) . x1 misses (the_Edges_of F) . x2 ) ) by Th70, Th71; :: thesis: ( ( for x1, x2 being Element of dom F st x1 <> x2 holds
( (the_Vertices_of F) . x1 misses (the_Vertices_of F) . x2 & (the_Edges_of F) . x1 misses (the_Edges_of F) . x2 ) ) implies ( F is vertex-disjoint & F is edge-disjoint ) )
assume A1: for x1, x2 being Element of dom F st x1 <> x2 holds
( (the_Vertices_of F) . x1 misses (the_Vertices_of F) . x2 & (the_Edges_of F) . x1 misses (the_Edges_of F) . x2 ) ; :: thesis: ( F is vertex-disjoint & F is edge-disjoint )
then for x1, x2 being Element of dom F st x1 <> x2 holds
(the_Vertices_of F) . x1 misses (the_Vertices_of F) . x2 ;
hence F is vertex-disjoint by Th70; :: thesis: F is edge-disjoint
for x1, x2 being Element of dom F st x1 <> x2 holds
(the_Edges_of F) . x1 misses (the_Edges_of F) . x2 by A1;
hence F is edge-disjoint by Th71; :: thesis: verum