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 :: thesis: for x being object st x in G2 .edgesBetween (X,Y) holds
x in G1 .edgesBetween (X,Y)

let x be object ; :: 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 Def30;
then x SJoins X,Y,G1 by Th72;
hence x in G1 .edgesBetween (X,Y) by Def30; :: thesis: verum

end;

hence G2 .edgesBetween (X,Y) c= G1 .edgesBetween (X,Y) ; :: thesis: G2 .edgesDBetween (X,Y) c= G1 .edgesDBetween (X,Y)

now :: thesis: for x being object st x in G2 .edgesDBetween (X,Y) holds
x in G1 .edgesDBetween (X,Y)

let x be object ; :: 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 Def31;
then x DSJoins X,Y,G1 by Th72;
hence x in G1 .edgesDBetween (X,Y) by Def31; :: thesis: verum

end;

hence G2 .edgesDBetween (X,Y) c= G1 .edgesDBetween (X,Y) ; :: thesis: verum