assume not the_Vertices_of S is empty ; :: thesis: contradiction
then consider V being object such that
A1: V in the_Vertices_of S by XBOOLE_0:def 1;
ex G being _Graph st
( G in S & V = the_Vertices_of G ) by A1, Def14;
hence contradiction ; :: thesis: verum