for G being _Graph
for S being Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for u, v being object st u in S & v in S holds
for e being object st e Joins u,v,G holds
e Joins u,v,H