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

assume A1: F is vertex-disjoint ; :: thesis: for x1, x2 being Element of dom F st x1 <> x2 holds
the_Vertices_of (F . x1) misses the_Vertices_of (F . x2)
let x1, x2 be Element of dom F; :: thesis: ( x1 <> x2 implies the_Vertices_of (F . x1) misses the_Vertices_of (F . x2) )
assume x1 <> x2 ; :: thesis: the_Vertices_of (F . x1) misses the_Vertices_of (F . x2)
then consider G1, G2 being _Graph such that
A2: ( G1 = F . x1 & G2 = F . x2 & the_Vertices_of G1 misses the_Vertices_of G2 ) by A1;
thus the_Vertices_of (F . x1) misses the_Vertices_of (F . x2) by A2; :: thesis: verum

end;

assume A3: for x1, x2 being Element of dom F st x1 <> x2 holds
the_Vertices_of (F . x1) misses the_Vertices_of (F . x2) ; :: thesis: F is vertex-disjoint
let x1, x2 be object ; :: according to GLIB_015:def 20 :: 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_Vertices_of G1 misses the_Vertices_of G2 ) )
assume A4: ( x1 in dom F & x2 in dom F & x1 <> x2 ) ; :: thesis: ex G1, G2 being _Graph st
( G1 = F . x1 & G2 = F . x2 & the_Vertices_of G1 misses the_Vertices_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_Vertices_of (F . y1) misses the_Vertices_of G2 )
take F . y2 ; :: thesis: ( F . y1 = F . x1 & F . y2 = F . x2 & the_Vertices_of (F . y1) misses the_Vertices_of (F . y2) )
thus ( F . y1 = F . x1 & F . y2 = F . x2 & the_Vertices_of (F . y1) misses the_Vertices_of (F . y2) ) by A3, A4; :: thesis: verum