let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for X, Y being set holds
( G2 .edgesBetween X,Y c= G1 .edgesBetween X,Y & G2 .edgesDBetween X,Y c= G1 .edgesDBetween X,Y )
let G2 be Subgraph of G1; :: thesis: for X, Y being set holds
( G2 .edgesBetween X,Y c= G1 .edgesBetween X,Y & G2 .edgesDBetween X,Y c= G1 .edgesDBetween X,Y )
let X, Y be set ; :: thesis: ( G2 .edgesBetween X,Y c= G1 .edgesBetween X,Y & G2 .edgesDBetween X,Y c= G1 .edgesDBetween X,Y )

now

let x be set ; :: thesis: ( x in G2 .edgesBetween X,Y implies x in G1 .edgesBetween X,Y )
assume x in G2 .edgesBetween X,Y ; :: thesis: x in G1 .edgesBetween X,Y
then x SJoins X,Y,G2 by Def32;
then x SJoins X,Y,G1 by Th75;
hence x in G1 .edgesBetween X,Y by Def32; :: thesis: verum

end;

hence G2 .edgesBetween X,Y c= G1 .edgesBetween X,Y by TARSKI:def 3; :: thesis: G2 .edgesDBetween X,Y c= G1 .edgesDBetween X,Y

now

let x be set ; :: thesis: ( x in G2 .edgesDBetween X,Y implies x in G1 .edgesDBetween X,Y )
assume x in G2 .edgesDBetween X,Y ; :: thesis: x in G1 .edgesDBetween X,Y
then x DSJoins X,Y,G2 by Def33;
then x DSJoins X,Y,G1 by Th75;
hence x in G1 .edgesDBetween X,Y by Def33; :: thesis: verum

end;

hence G2 .edgesDBetween X,Y c= G1 .edgesDBetween X,Y by TARSKI:def 3; :: thesis: verum