let F be non empty Graph-yielding Function; :: thesis: ( F is edge-disjoint iff for x1, x2 being Element of dom F st x1 <> x2 holds
(the_Edges_of F) . x1 misses (the_Edges_of F) . x2 )

hereby :: thesis: ( ( for x1, x2 being Element of dom F st x1 <> x2 holds
(the_Edges_of F) . x1 misses (the_Edges_of F) . x2 ) implies F is edge-disjoint )

assume A1: F is edge-disjoint ; :: thesis: for x1, x2 being Element of dom F st x1 <> x2 holds
(the_Edges_of F) . x1 misses (the_Edges_of F) . x2
let x1, x2 be Element of dom F; :: thesis: ( x1 <> x2 implies (the_Edges_of F) . x1 misses (the_Edges_of F) . x2 )
assume A2: x1 <> x2 ; :: thesis: (the_Edges_of F) . x1 misses (the_Edges_of F) . x2
( (the_Edges_of F) . x1 = the_Edges_of (F . x1) & (the_Edges_of F) . x2 = the_Edges_of (F . x2) ) by Def9;
hence (the_Edges_of F) . x1 misses (the_Edges_of F) . x2 by A1, A2; :: thesis: verum

end;

assume A3: for x1, x2 being Element of dom F st x1 <> x2 holds
(the_Edges_of F) . x1 misses (the_Edges_of F) . x2 ; :: thesis: F is edge-disjoint
let x1, x2 be Element of dom F; :: according to GLIB_015:def 23 :: thesis: ( x1 <> x2 implies the_Edges_of (F . x1) misses the_Edges_of (F . x2) )
assume A4: x1 <> x2 ; :: thesis: the_Edges_of (F . x1) misses the_Edges_of (F . x2)
( (the_Edges_of F) . x1 = the_Edges_of (F . x1) & (the_Edges_of F) . x2 = the_Edges_of (F . x2) ) by Def9;
hence the_Edges_of (F . x1) misses the_Edges_of (F . x2) by A3, A4; :: thesis: verum