now :: thesis: for f, g being Function st f in the_Target_of S & g in the_Target_of S holds
f tolerates g

let f, g be Function; :: thesis: ( f in the_Target_of S & g in the_Target_of S implies f tolerates g )
assume A4: ( f in the_Target_of S & g in the_Target_of S ) ; :: thesis: f tolerates g
then consider G1 being _Graph such that
A5: ( G1 in S & f = the_Target_of G1 ) by Def17;
consider G2 being _Graph such that
A6: ( G2 in S & g = the_Target_of G2 ) by A4, Def17;
G1 tolerates G2 by A5, A6, Def23;
hence f tolerates g by A5, A6; :: thesis: verum

end;

hence the_Target_of S is compatible by COMPUT_1:def 1; :: thesis: verum