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