theorem Th39: :: GLENUM00:39

for G being _Graph
for H being Subgraph of G holds [(H | _GraphSelectors),(G | _GraphSelectors)] in SubgraphRel G