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

let x, y be object ; :: thesis: ( x in the_Target_of S & y in the_Target_of S implies x = y )
assume A10: ( x in the_Target_of S & y in the_Target_of S ) ; :: thesis: x = y
then consider G1 being _Graph such that
A11: ( G1 in S & x = the_Target_of G1 ) by Def17;
consider G2 being _Graph such that
A12: ( G2 in S & y = the_Target_of G2 ) by A10, Def17;
thus x = y by A11, A12, ZFMISC_1:def 10; :: thesis: verum

end;

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