let G1, G2 be _Graph; :: thesis:
let e be set ; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume that
A1: v1 = v2 and
A2: G1 == G2 ; :: thesis:
thus A3: v1 .edgesIn() = v2 .edgesIn() by A1, A2, Th90; :: thesis:
thus A4: v1 .edgesOut() = v2 .edgesOut() by A1, A2, Th90; :: thesis:
thus v1 .edgesInOut() = v2 .edgesInOut() by A1, A2, Th90; :: thesis:

suppose A5: ( e in the_Edges_of G1 & (the_Target_of G1) . e = v1 ) ; :: thesis:

then A6: ( e in the_Edges_of G2 & (the_Target_of G2) . e = v2 ) by A1, A2;
thus v1 .adj e = (the_Source_of G1) . e by A5, Def41
.= (the_Source_of G2) . e by A2
.= v2 .adj e by A6, Def41 ; :: thesis:

end;

suppose A7: ( e in the_Edges_of G1 & (the_Source_of G1) . e = v1 & not (the_Target_of G1) . e = v1 ) ; :: thesis:

then A8: not (the_Target_of G2) . e = v2 by A1, A2;
A9: ( e in the_Edges_of G2 & (the_Source_of G2) . e = v2 ) by A1, A2, A7;
thus v1 .adj e = (the_Target_of G1) . e by A7, Def41
.= (the_Target_of G2) . e by A2
.= v2 .adj e by A9, A8, Def41 ; :: thesis:

end;

suppose A10: ( ( not e in the_Edges_of G1 or not (the_Target_of G1) . e = v1 ) & ( not e in the_Edges_of G1 or not (the_Source_of G1) . e = v1 or (the_Target_of G1) . e = v1 ) ) ; :: thesis:

then A11: ( ( not e in the_Edges_of G2 or not (the_Target_of G2) . e = v2 ) & ( not e in the_Edges_of G2 or not (the_Source_of G2) . e = v2 or (the_Target_of G2) . e = v2 ) ) by A1, A2;
thus v1 .adj e = v2 by A1, A10, Def41
.= v2 .adj e by A11, Def41 ; :: thesis:

end;

end;

end;

hence v1 .adj e = v2 .adj e ; :: thesis:
thus v1 .inDegree() = v2 .inDegree() by A1, A2, Th90; :: thesis:
thus v1 .outDegree() = v2 .outDegree() by A1, A2, Th90; :: thesis:
hence v1 .degree() = v2 .degree() by A1, A2, Th90; :: thesis:
thus v1 .inNeighbors() = v2 .inNeighbors() by A2, A3; :: thesis:
thus v1 .outNeighbors() = v2 .outNeighbors() by A2, A4; :: thesis:
hence v1 .allNeighbors() = v2 .allNeighbors() by A2, A3; :: thesis: