let S1, S2 be Graph-membered set ; :: thesis: ( S1 \/ S2 is edge-disjoint implies ( S1 is edge-disjoint & S2 is edge-disjoint ) )
assume A1: S1 \/ S2 is edge-disjoint ; :: thesis: ( S1 is edge-disjoint & S2 is edge-disjoint )

hereby :: according to GLIB_015:def 19 :: thesis: S2 is edge-disjoint

let G1, G2 be _Graph; :: thesis: ( G1 in S1 & G2 in S1 & G1 <> G2 implies the_Edges_of G1 misses the_Edges_of G2 )
assume ( G1 in S1 & G2 in S1 & G1 <> G2 ) ; :: thesis: the_Edges_of G1 misses the_Edges_of G2
then ( G1 in S1 \/ S2 & G2 in S1 \/ S2 & G1 <> G2 ) by XBOOLE_0:def 3;
hence the_Edges_of G1 misses the_Edges_of G2 by A1; :: thesis: verum

end;

let G1, G2 be _Graph; :: according to GLIB_015:def 19 :: thesis: ( G1 in S2 & G2 in S2 & G1 <> G2 implies the_Edges_of G1 misses the_Edges_of G2 )
assume ( G1 in S2 & G2 in S2 & G1 <> G2 ) ; :: thesis: the_Edges_of G1 misses the_Edges_of G2
then ( G1 in S1 \/ S2 & G2 in S1 \/ S2 & G1 <> G2 ) by XBOOLE_0:def 3;
hence the_Edges_of G1 misses the_Edges_of G2 by A1; :: thesis: verum