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:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume A2: x in v2 .edgesIn() ; :: thesis:
v2 .edgesIn() c= v1 .edgesIn() by A1, Th78;
hence x in (v1 .edgesIn()) /\ (the_Edges_of G2) by A2, XBOOLE_0:def 4; :: thesis:

end;

assume A3: x in (v1 .edgesIn()) /\ (the_Edges_of G2) ; :: thesis:
then A4: x in the_Edges_of G2 by XBOOLE_0:def 4;
x in v1 .edgesIn() by A3, XBOOLE_0:def 4;
then (the_Target_of G1) . x = v1 by Lm7;
then (the_Target_of G2) . x = v2 by A1, A4, Def32;
hence x in v2 .edgesIn() by A4, Lm7; :: thesis:

end;

hence A5: v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) by TARSKI:2; :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume A6: x in v2 .edgesOut() ; :: thesis:
v2 .edgesOut() c= v1 .edgesOut() by A1, Th78;
hence x in (v1 .edgesOut()) /\ (the_Edges_of G2) by A6, XBOOLE_0:def 4; :: thesis:

end;

assume A7: x in (v1 .edgesOut()) /\ (the_Edges_of G2) ; :: thesis:
then A8: x in the_Edges_of G2 by XBOOLE_0:def 4;
x in v1 .edgesOut() by A7, XBOOLE_0:def 4;
then (the_Source_of G1) . x = v1 by Lm8;
then (the_Source_of G2) . x = v2 by A1, A8, Def32;
hence x in v2 .edgesOut() by A8, Lm8; :: thesis:

end;

hence A9: v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) by TARSKI:2; :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume A10: x in (v1 .edgesInOut()) /\ (the_Edges_of G2) ; :: thesis:
then A11: x in the_Edges_of G2 by XBOOLE_0:def 4;
A12: x in v1 .edgesInOut() by A10, XBOOLE_0:def 4;

now :: thesis:

per cases by A12, XBOOLE_0:def 3;

suppose x in v1 .edgesIn() ; :: thesis:

then x in (v1 .edgesIn()) /\ (the_Edges_of G2) by A11, XBOOLE_0:def 4;
hence x in v2 .edgesInOut() by A5, XBOOLE_0:def 3; :: thesis:

end;

suppose x in v1 .edgesOut() ; :: thesis:

then x in (v1 .edgesOut()) /\ (the_Edges_of G2) by A11, XBOOLE_0:def 4;
hence x in v2 .edgesInOut() by A9, XBOOLE_0:def 3; :: thesis:

end;

end;

end;

hence x in v2 .edgesInOut() ; :: thesis:

end;

assume A13: x in v2 .edgesInOut() ; :: thesis:

now :: thesis:

per cases by A5, A9, A13, XBOOLE_0:def 3;

suppose A14: x in (v1 .edgesIn()) /\ (the_Edges_of G2) ; :: thesis:

then x in v1 .edgesIn() by XBOOLE_0:def 4;
then A15: x in (v1 .edgesIn()) \/ (v1 .edgesOut()) by XBOOLE_0:def 3;
x in the_Edges_of G2 by A14, XBOOLE_0:def 4;
hence x in (v1 .edgesInOut()) /\ (the_Edges_of G2) by A15, XBOOLE_0:def 4; :: thesis:

end;

suppose A16: x in (v1 .edgesOut()) /\ (the_Edges_of G2) ; :: thesis:

then x in v1 .edgesOut() by XBOOLE_0:def 4;
then A17: x in (v1 .edgesIn()) \/ (v1 .edgesOut()) by XBOOLE_0:def 3;
x in the_Edges_of G2 by A16, XBOOLE_0:def 4;
hence x in (v1 .edgesInOut()) /\ (the_Edges_of G2) by A17, XBOOLE_0:def 4; :: thesis:

end;

end;

end;

hence x in (v1 .edgesInOut()) /\ (the_Edges_of G2) ; :: thesis:

end;

hence v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) by TARSKI:2; :: thesis: