:: deftheorem Def5 defines SG2SGFunc GLENUM00:def 5 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for b₄ being Function of (G1 .allSG()),(G2 .allSG()) holds
( b₄ = SG2SGFunc F iff for H being plain Subgraph of G1 holds b₄ . H = rng (F | H) );