theorem :: GLIB_000:127

for G being _trivial _Graph
for H being _Graph st the_Vertices_of H c= the_Vertices_of G & the_Edges_of H c= the_Edges_of G holds
( H is _trivial & H is Subgraph of G )