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

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

end;

hence A3: G2 .edgesInto X c= G1 .edgesInto X by TARSKI:def 3; :: thesis:

let e be set ; :: thesis:
assume A4: e in G2 .edgesOutOf X ; :: thesis:
then A5: ( e in the_Edges_of G2 & (the_Source_of G2) . e in X ) by Def29;
(the_Source_of G2) . e = (the_Source_of G1) . e by A4, Def34;
hence e in G1 .edgesOutOf X by A5, Def29; :: thesis:

end;

hence A6: G2 .edgesOutOf X c= G1 .edgesOutOf X by TARSKI:def 3; :: thesis:
A7: G2 .edgesInto X c= G1 .edgesInOut X by A3, XBOOLE_1:10;
G2 .edgesOutOf X c= G1 .edgesInOut X by A6, XBOOLE_1:10;
hence G2 .edgesInOut X c= G1 .edgesInOut X by A7, XBOOLE_1:8; :: thesis:
thus G2 .edgesBetween X c= G1 .edgesBetween X by A3, A6, XBOOLE_1:27; :: thesis: