theorem :: GLIB_000:5

for GS being GraphStruct holds
( GS is [Graph-like] iff ( _GraphSelectors c= dom GS & not the_Vertices_of GS is empty & the_Source_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) & the_Target_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) ) ) by Lm1;