theorem Th5: :: GLIB_014:5

for G being _Graph holds
( the_Vertices_of {G} = {(the_Vertices_of G)} & the_Edges_of {G} = {(the_Edges_of G)} & the_Source_of {G} = {(the_Source_of G)} & the_Target_of {G} = {(the_Target_of G)} )