take G ; :: thesis: ( the_Vertices_of G c= the_Vertices_of G & the_Edges_of G c= the_Edges_of G & ( for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of G) . e & (the_Target_of G) . e = (the_Target_of G) . e ) ) )
thus ( the_Vertices_of G c= the_Vertices_of G & the_Edges_of G c= the_Edges_of G & ( for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of G) . e & (the_Target_of G) . e = (the_Target_of G) . e ) ) ) ; :: thesis: verum