let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2
for e being set st v1 = v2 & e in the_Edges_of G2 holds
v1 .adj e = v2 .adj e
let G2 be Subgraph of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2
for e being set st v1 = v2 & e in the_Edges_of G2 holds
v1 .adj e = v2 .adj e
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2
for e being set st v1 = v2 & e in the_Edges_of G2 holds
v1 .adj e = v2 .adj e
let v2 be Vertex of G2; :: thesis: for e being set st v1 = v2 & e in the_Edges_of G2 holds
v1 .adj e = v2 .adj e
let e be set ; :: thesis: ( v1 = v2 & e in the_Edges_of G2 implies v1 .adj e = v2 .adj e )
assume that
A1: v1 = v2 and
A2: e in the_Edges_of G2 ; :: thesis: v1 .adj e = v2 .adj e
A3: ( (the_Source_of G2) . e = (the_Source_of G1) . e & (the_Target_of G2) . e = (the_Target_of G1) . e ) by A2, Def32;

now :: thesis: v1 .adj e = v2 .adj e

per cases ( (the_Target_of G1) . e = v1 or ( (the_Source_of G1) . e = v1 & (the_Target_of G1) . e <> v1 ) or ( (the_Source_of G1) . e <> v1 & (the_Target_of G1) . e <> v1 ) ) ;

suppose A4: (the_Target_of G1) . e = v1 ; :: thesis: v1 .adj e = v2 .adj e

hence v1 .adj e = (the_Source_of G1) . e by A2, Def41
.= v2 .adj e by A1, A2, A3, A4, Def41 ;
:: thesis: verum

end;

suppose A5: ( (the_Source_of G1) . e = v1 & (the_Target_of G1) . e <> v1 ) ; :: thesis: v1 .adj e = v2 .adj e

hence v1 .adj e = (the_Target_of G1) . e by A2, Def41
.= v2 .adj e by A1, A2, A3, A5, Def41 ;
:: thesis: verum

end;

suppose A6: ( (the_Source_of G1) . e <> v1 & (the_Target_of G1) . e <> v1 ) ; :: thesis: v1 .adj e = v2 .adj e

hence v1 .adj e = v2 by A1, Def41
.= v2 .adj e by A1, A3, A6, Def41 ;
:: thesis: verum

end;

end;

end;

hence v1 .adj e = v2 .adj e ; :: thesis: verum