let G be _Graph; :: thesis: for H being Subgraph of G holds [(H | _GraphSelectors),(G | _GraphSelectors)] in SubgraphRel G
let H be Subgraph of G; :: thesis: [(H | _GraphSelectors),(G | _GraphSelectors)] in SubgraphRel G
A1: ( H | _GraphSelectors == H & G | _GraphSelectors == G ) by GLIB_000:128;
A2: ( H | _GraphSelectors in G .allSG() & G | _GraphSelectors in G .allSG() ) by Th2, Th3;
H | _GraphSelectors is Subgraph of G by A1, GLIB_000:92;
then H | _GraphSelectors is Subgraph of G | _GraphSelectors by A1, GLIB_000:91;
hence [(H | _GraphSelectors),(G | _GraphSelectors)] in SubgraphRel G by A2, Def6; :: thesis: verum