theorem Th7: :: GLIB_014:7

for S being Graph-membered set holds
( card (the_Vertices_of S) c= card S & card (the_Edges_of S) c= card S & card (the_Source_of S) c= card S & card (the_Target_of S) c= card S )