let G1, G2 be _Graph; :: according to GLIB_015:def 19 :: thesis: ( G1 in rng F & G2 in rng F & G1 <> G2 implies the_Edges_of G1 misses the_Edges_of G2 )
assume A1: ( G1 in rng F & G2 in rng F & G1 <> G2 ) ; :: thesis: the_Edges_of G1 misses the_Edges_of G2
then consider x1 being object such that
A2: ( x1 in dom F & F . x1 = G1 ) by FUNCT_1:def 3;
consider x2 being object such that
A3: ( x2 in dom F & F . x2 = G2 ) by A1, FUNCT_1:def 3;
consider G3, G4 being _Graph such that
A4: ( G3 = F . x1 & G4 = F . x2 & the_Edges_of G3 misses the_Edges_of G4 ) by A1, A2, A3, Def21;
thus the_Edges_of G1 misses the_Edges_of G2 by A2, A3, A4; :: thesis: verum