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