let G1 be _Graph; :: thesis:
let G2 be Subgraph of G1; :: thesis:
let X be set ; :: thesis:

now :: thesis:

let e be object ; :: thesis:
assume A1: e in G2 .edgesInto X ; :: thesis:
then A2: (the_Target_of G2) . e = (the_Target_of G1) . e by Def32;
( e in the_Edges_of G2 & (the_Target_of G2) . e in X ) by A1, Def26;
hence e in G1 .edgesInto X by A2, Def26; :: thesis:

end;

hence A3: G2 .edgesInto X c= G1 .edgesInto X ; :: thesis:
then A4: G2 .edgesInto X c= G1 .edgesInOut X by XBOOLE_1:10;

now :: thesis:

let e be object ; :: thesis:
assume A5: e in G2 .edgesOutOf X ; :: thesis:
then A6: (the_Source_of G2) . e = (the_Source_of G1) . e by Def32;
( e in the_Edges_of G2 & (the_Source_of G2) . e in X ) by A5, Def27;
hence e in G1 .edgesOutOf X by A6, Def27; :: thesis:

end;

hence A7: G2 .edgesOutOf X c= G1 .edgesOutOf X ; :: thesis:
then G2 .edgesOutOf X c= G1 .edgesInOut X by XBOOLE_1:10;
hence G2 .edgesInOut X c= G1 .edgesInOut X by A4, XBOOLE_1:8; :: thesis:
thus G2 .edgesBetween X c= G1 .edgesBetween X by A3, A7, XBOOLE_1:27; :: thesis: