let G1 be _Graph; :: thesis: for G2, G3 being Subgraph of G1 holds G2 tolerates G3
let G2, G3 be Subgraph of G1; :: thesis: G2 tolerates G3
A1: ( G1 is Supergraph of G2 & G1 is Supergraph of G3 ) by GLIB_006:57;
( the_Source_of G2 c= the_Source_of G1 & the_Source_of G3 c= the_Source_of G1 ) by A1, GLIB_006:64;
hence the_Source_of G2 tolerates the_Source_of G3 by PARTFUN1:52; :: according to GLIB_014:def 22 :: thesis: the_Target_of G2 tolerates the_Target_of G3
( the_Target_of G2 c= the_Target_of G1 & the_Target_of G3 c= the_Target_of G1 ) by A1, GLIB_006:64;
hence the_Target_of G2 tolerates the_Target_of G3 by PARTFUN1:52; :: thesis: verum