let S be Graph-membered set ; :: thesis: ( S is edge-disjoint implies S is \/-tolerating )
assume A2: S is edge-disjoint ; :: thesis: S is \/-tolerating

now :: thesis: for G1, G2 being _Graph st G1 in S & G2 in S holds
G1 tolerates G2

let G1, G2 be _Graph; :: thesis: ( G1 in S & G2 in S implies b₁ tolerates b₂ )
assume A3: ( G1 in S & G2 in S ) ; :: thesis: b₁ tolerates b₂

per cases ( G1 = G2 or G1 <> G2 ) ;

suppose G1 = G2 ; :: thesis: b₁ tolerates b₂

hence G1 tolerates G2 ; :: thesis: verum

end;

suppose G1 <> G2 ; :: thesis: b₁ tolerates b₂

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

end;

end;

end;

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