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

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