let S be Graph-membered set ; ( S is vertex-disjoint & S is \/-tolerating implies S is edge-disjoint )
assume A4:
( S is vertex-disjoint & S is \/-tolerating )
; S is edge-disjoint
let G1, G2 be _Graph; GLIB_015:def 19 ( 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 )
; 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) <> {}
;
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;
verum
end;
hence
the_Edges_of G1 misses the_Edges_of G2
by XBOOLE_0:def 7; verum