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 A2: x in v2 .edgesIn() ; :: thesis:
then (the_Target_of G2) . x = v2 by Lm8;
then A3: (the_Target_of G1) . x = v1 by A1, A2, Def34;
x in the_Edges_of G2 by A2;
hence x in v1 .edgesIn() by A3, Lm8; :: thesis:

end;

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

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

end;

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

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

end;

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