1 <= len (W .vertexSeq()) by GLIB_001:67;
then W .vertexSeq() <> {} ;
then rng (W .vertexSeq()) <> {} ;
hence not W .vertices() is empty by GLIB_001:def 16; :: thesis: verum