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

let x, y be object ; :: thesis: ( x in the_Edges_of S & y in the_Edges_of S implies x = y )
assume A4: ( x in the_Edges_of S & y in the_Edges_of S ) ; :: thesis: x = y
then consider G1 being _Graph such that
A5: ( G1 in S & x = the_Edges_of G1 ) by Def15;
consider G2 being _Graph such that
A6: ( G2 in S & y = the_Edges_of G2 ) by A4, Def15;
thus x = y by A5, A6, ZFMISC_1:def 10; :: thesis: verum

end;

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