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 A5: 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 x1 <> x2 ; :: thesis: the_Edges_of (F . x1) misses the_Edges_of (F . x2)
then consider G1, G2 being _Graph such that
A6: ( G1 = F . x1 & G2 = F . x2 & the_Edges_of G1 misses the_Edges_of G2 ) by A5;
thus the_Edges_of (F . x1) misses the_Edges_of (F . x2) by A6; :: thesis: verum
end;
assume A7: 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 object ; :: according to GLIB_015:def 21 :: thesis: ( x1 in dom F & x2 in dom F & x1 <> x2 implies ex G1, G2 being _Graph st
( G1 = F . x1 & G2 = F . x2 & the_Edges_of G1 misses the_Edges_of G2 ) )
assume A8: ( x1 in dom F & x2 in dom F & x1 <> x2 ) ; :: thesis: ex G1, G2 being _Graph st
( G1 = F . x1 & G2 = F . x2 & the_Edges_of G1 misses the_Edges_of G2 )
then reconsider y1 = x1, y2 = x2 as Element of dom F ;
take F . y1 ; :: thesis: ex G2 being _Graph st
( F . y1 = F . x1 & G2 = F . x2 & the_Edges_of (F . y1) misses the_Edges_of G2 )
take F . y2 ; :: thesis: ( F . y1 = F . x1 & F . y2 = F . x2 & the_Edges_of (F . y1) misses the_Edges_of (F . y2) )
thus ( F . y1 = F . x1 & F . y2 = F . x2 & the_Edges_of (F . y1) misses the_Edges_of (F . y2) ) by A7, A8; :: thesis: verum