:: deftheorem defines | GLIB_010:def 31 :
for G1, G2 being _Graph
for H being Subgraph of G1
for F being PGraphMapping of G1,G2 holds F | H = [((F _V) | (the_Vertices_of H)),((F _E) | (the_Edges_of H))];