let G1, G2 be _Graph; :: thesis:

hereby :: thesis:

assume A1: {G1,G2} is edge-disjoint ; :: thesis:
assume A2: G1 <> G2 ; :: thesis:
( G1 in {G1,G2} & G2 in {G1,G2} ) by TARSKI:def 2;
hence the_Edges_of G1 misses the_Edges_of G2 by A1, A2; :: thesis:

end;

assume ( G1 = G2 or the_Edges_of G1 misses the_Edges_of G2 ) ; :: thesis:

suppose G1 = G2 ; :: thesis:

then {G1,G2} = {G1} by ENUMSET1:29;
hence {G1,G2} is edge-disjoint ; :: thesis:

end;

suppose A3: the_Edges_of G1 misses the_Edges_of G2 ; :: thesis:

let G3, G4 be _Graph; :: according to GLIB_015:def 19 :: thesis:
assume ( G3 in {G1,G2} & G4 in {G1,G2} & G3 <> G4 ) ; :: thesis:
then ( ( G3 = G1 or G3 = G2 ) & ( G4 = G1 or G4 = G2 ) & G3 <> G4 ) by TARSKI:def 2;
hence the_Edges_of G3 misses the_Edges_of G4 by A3; :: thesis:

end;

end;