let S be Graph-membered set ; :: thesis: ( S is vertex-disjoint & S is \/-tolerating implies S is edge-disjoint )
assume A4: ( S is vertex-disjoint & S is \/-tolerating ) ; :: thesis: S is edge-disjoint
let G1, G2 be _Graph; :: according to GLIB_015:def 19 :: thesis: ( G1 in S & G2 in S & G1 <> G2 implies the_Edges_of G1 misses the_Edges_of G2 )
assume A5: ( G1 in S & G2 in S & G1 <> G2 ) ; :: thesis: the_Edges_of G1 misses the_Edges_of G2
(the_Edges_of G1) /\ (the_Edges_of G2) = {}

proof

assume (the_Edges_of G1) /\ (the_Edges_of G2) <> {} ; :: thesis: contradiction
then consider e being object such that
A6: e in (the_Edges_of G1) /\ (the_Edges_of G2) by XBOOLE_0:def 1;
set v1 = (the_Source_of G1) . e;
set w1 = (the_Target_of G1) . e;
set v2 = (the_Source_of G2) . e;
set w2 = (the_Target_of G2) . e;
( e in the_Edges_of G1 & e in the_Edges_of G2 ) by A6, XBOOLE_0:def 4;
then A7: ( e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 & e DJoins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 ) by GLIB_000:def 14;
G1 tolerates G2 by A4, A5, GLIB_014:def 23;
then A8: (the_Source_of G1) . e = (the_Source_of G2) . e by A7, GLIB_014:17;
( e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 & e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 ) by A7, GLIB_000:16;
then ( (the_Source_of G1) . e in the_Vertices_of G1 & (the_Source_of G2) . e in the_Vertices_of G2 ) by GLIB_000:13;
hence contradiction by A4, A5, A8, XBOOLE_0:3; :: thesis: verum

end;

hence the_Edges_of G1 misses the_Edges_of G2 by XBOOLE_0:def 7; :: thesis: verum