let S be Graph-membered set ; :: thesis:
assume A2: S is edge-disjoint ; :: thesis:

let G1, G2 be _Graph; :: thesis:
assume A3: ( G1 in S & G2 in S ) ; :: thesis:

suppose G1 = G2 ; :: thesis:

hence G1 tolerates G2 ; :: thesis:

end;

suppose G1 <> G2 ; :: thesis:

then the_Edges_of G1 misses the_Edges_of G2 by A2, A3;
hence G1 tolerates G2 by GLIB_014:12; :: thesis:

end;

end;

end;

hence S is \/-tolerating by GLIB_014:def 23; :: thesis: