for G being _Graph
for G1, G2 being Subgraph of G holds
( not G1 c< G2 or ex v being object st
( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being object st
( e in the_Edges_of G2 & not e in the_Edges_of G1 ) )