now :: thesis: for x, y being object st x in the_Source_of S & y in the_Source_of S holds
x = y

let x, y be object ; :: thesis: ( x in the_Source_of S & y in the_Source_of S implies x = y )
assume A7: ( x in the_Source_of S & y in the_Source_of S ) ; :: thesis: x = y
then consider G1 being _Graph such that
A8: ( G1 in S & x = the_Source_of G1 ) by Def16;
consider G2 being _Graph such that
A9: ( G2 in S & y = the_Source_of G2 ) by A7, Def16;
thus x = y by A8, A9, ZFMISC_1:def 10; :: thesis: verum

end;

hence the_Source_of S is trivial by ZFMISC_1:def 10; :: thesis: verum