let G be _Graph; :: thesis: for H being Subgraph of G holds SubgraphRel H = (SubgraphRel G) |_2 (H .allSG())
let H be Subgraph of G; :: thesis: SubgraphRel H = (SubgraphRel G) |_2 (H .allSG())
A1: H .allSG() c= G .allSG() by Th29;
reconsider R = (SubgraphRel G) |_2 (H .allSG()) as Relation of (H .allSG()) ;

now :: thesis: for H1, H2 being Element of H .allSG() holds
( ( [H1,H2] in SubgraphRel H implies [H1,H2] in R ) & ( [H1,H2] in R implies [H1,H2] in SubgraphRel H ) )

let H1, H2 be Element of H .allSG() ; :: thesis: ( ( [H1,H2] in SubgraphRel H implies [H1,H2] in R ) & ( [H1,H2] in R implies [H1,H2] in SubgraphRel H ) )

hereby :: thesis: ( [H1,H2] in R implies [H1,H2] in SubgraphRel H )

assume [H1,H2] in SubgraphRel H ; :: thesis: [H1,H2] in R
then A2: H1 is Subgraph of H2 by Def6;
( H1 in G .allSG() & H2 in G .allSG() ) by A1, TARSKI:def 3;
then [H1,H2] in SubgraphRel G by A2, Def6;
hence [H1,H2] in R by MMLQUER2:4; :: thesis: verum

end;

assume [H1,H2] in R ; :: thesis: [H1,H2] in SubgraphRel H
then A3: [H1,H2] in SubgraphRel G by MMLQUER2:4;
then ( H1 in field (SubgraphRel G) & H2 in field (SubgraphRel G) ) by RELAT_1:15;
then ( H1 in G .allSG() & H2 in G .allSG() ) by Th40;
then H1 is Subgraph of H2 by A3, Def6;
hence [H1,H2] in SubgraphRel H by Def6; :: thesis: verum

end;

hence SubgraphRel H = (SubgraphRel G) |_2 (H .allSG()) by RELSET_1:def 2; :: thesis: verum