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

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