let G1, G2 be _Graph; :: thesis: ( the_Edges_of G1 misses the_Edges_of G2 implies G1 tolerates G2 )
assume A1: the_Edges_of G1 misses the_Edges_of G2 ; :: thesis: G1 tolerates G2
then dom (the_Source_of G1) misses the_Edges_of G2 by FUNCT_2:def 1;
then dom (the_Source_of G1) misses dom (the_Source_of G2) by FUNCT_2:def 1;
hence the_Source_of G1 tolerates the_Source_of G2 by PARTFUN1:56; :: according to GLIB_014:def 22 :: thesis: the_Target_of G1 tolerates the_Target_of G2
dom (the_Target_of G1) misses the_Edges_of G2 by A1, FUNCT_2:def 1;
then dom (the_Target_of G1) misses dom (the_Target_of G2) by FUNCT_2:def 1;
hence the_Target_of G1 tolerates the_Target_of G2 by PARTFUN1:56; :: thesis: verum