set G = the _Graph;
take the _Graph .set (ELabelSelector,(id (the_Edges_of the _Graph))) ; :: thesis: ( the _Graph .set (ELabelSelector,(id (the_Edges_of the _Graph))) is elabel-distinct & the _Graph .set (ELabelSelector,(id (the_Edges_of the _Graph))) is elabel-full )
thus ( the _Graph .set (ELabelSelector,(id (the_Edges_of the _Graph))) is elabel-distinct & the _Graph .set (ELabelSelector,(id (the_Edges_of the _Graph))) is elabel-full ) ; :: thesis: verum