set G = the _Graph;
take the _Graph .set (VLabelSelector,(id (the_Vertices_of the _Graph))) ; :: thesis: ( the _Graph .set (VLabelSelector,(id (the_Vertices_of the _Graph))) is vlabel-distinct & the _Graph .set (VLabelSelector,(id (the_Vertices_of the _Graph))) is vlabel-full )
thus ( the _Graph .set (VLabelSelector,(id (the_Vertices_of the _Graph))) is vlabel-distinct & the _Graph .set (VLabelSelector,(id (the_Vertices_of the _Graph))) is vlabel-full ) ; :: thesis: verum