let G1 be _Graph; :: thesis:
let G2 be Subgraph of G1; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: v1 = v2 ; :: thesis:

let x be set ; :: thesis:
assume x in v2 .edgesIn() ; :: thesis:
then A2: ( x in the_Edges_of G2 & (the_Target_of G2) . x = v2 ) by Lm8;
then (the_Target_of G1) . x = v1 by A1, Def34;
hence x in v1 .edgesIn() by A2, Lm8; :: thesis:

end;

hence v2 .edgesIn() c= v1 .edgesIn() by TARSKI:def 3; :: thesis:

let x be set ; :: thesis:
assume x in v2 .edgesOut() ; :: thesis:
then A3: ( x in the_Edges_of G2 & (the_Source_of G2) . x = v2 ) by Lm9;
then (the_Source_of G1) . x = v1 by A1, Def34;
hence x in v1 .edgesOut() by A3, Lm9; :: thesis:

end;

hence v2 .edgesOut() c= v1 .edgesOut() by TARSKI:def 3; :: thesis:

let x be set ; :: thesis:
assume x in v2 .edgesInOut() ; :: thesis:
then A4: ( x in the_Edges_of G2 & ( (the_Source_of G2) . x = v2 or (the_Target_of G2) . x = v2 ) ) by Th64;
then ( (the_Source_of G1) . x = v1 or (the_Target_of G1) . x = v1 ) by A1, Def34;
hence x in v1 .edgesInOut() by A4, Th64; :: thesis:

end;

hence v2 .edgesInOut() c= v1 .edgesInOut() by TARSKI:def 3; :: thesis: