now :: thesis: for x, y being object st x in the_Vertices_of S & y in the_Vertices_of S holds
x = y
let x, y be object ; :: thesis: ( x in the_Vertices_of S & y in the_Vertices_of S implies x = y )
assume A1: ( x in the_Vertices_of S & y in the_Vertices_of S ) ; :: thesis: x = y
then consider G1 being _Graph such that
A2: ( G1 in S & x = the_Vertices_of G1 ) by Def14;
consider G2 being _Graph such that
A3: ( G2 in S & y = the_Vertices_of G2 ) by A1, Def14;
thus x = y by A2, A3, ZFMISC_1:def 10; :: thesis: verum
end;
hence the_Vertices_of S is trivial by ZFMISC_1:def 10; :: thesis: verum