now :: thesis: for f, g being Function st f in the_Source_of S & g in the_Source_of S holds
f tolerates g
let f, g be Function; :: thesis: ( f in the_Source_of S & g in the_Source_of S implies f tolerates g )
assume A1: ( f in the_Source_of S & g in the_Source_of S ) ; :: thesis: f tolerates g
then consider G1 being _Graph such that
A2: ( G1 in S & f = the_Source_of G1 ) by Def16;
consider G2 being _Graph such that
A3: ( G2 in S & g = the_Source_of G2 ) by A1, Def16;
G1 tolerates G2 by A2, A3, Def23;
hence f tolerates g by A2, A3; :: thesis: verum
end;
hence the_Source_of S is compatible by COMPUT_1:def 1; :: thesis: verum