let G1, G2 be _Graph; :: according to GLIB_014:def 23 :: thesis: ( G1 in S1 /\ S2 & G2 in S1 /\ S2 implies G1 tolerates G2 )
assume ( G1 in S1 /\ S2 & G2 in S1 /\ S2 ) ; :: thesis: G1 tolerates G2
then ( G1 in S1 & G2 in S1 ) by XBOOLE_0:def 4;
hence G1 tolerates G2 by Def23; :: thesis: verum