for G1 being edgeless _Graph
for G2 being _Graph holds
( G1 is Subgraph of G2 iff the_Vertices_of G1 c= the_Vertices_of G2 )