let G be _Graph; :: thesis:
let v1, v2 be Vertex of G; :: thesis:
let e be object ; :: thesis:
assume A1: e Joins v1,v2,G ; :: thesis:
then A2: e in v1 .edgesInOut() by Th62;

now :: thesis:

per cases ) . e = v2 & (the_Target_of G) . e = v1 ) or ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = v2 ) ) by A1;

suppose A3: ( (the_Source_of G) . e = v2 & (the_Target_of G) . e = v1 ) ; :: thesis:

hence v1 .adj e = v2 by A2, Def41; :: thesis:

now :: thesis:

per cases ;

suppose v1 = v2 ; :: thesis:

hence v2 .adj e = v1 by A2, A3, Def41; :: thesis:

end;

suppose v1 <> v2 ; :: thesis:

hence v2 .adj e = v1 by A2, A3, Def41; :: thesis:

end;

end;

end;

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

end;

suppose A4: ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = v2 ) ; :: thesis:

now :: thesis:

per cases ;

suppose v1 = v2 ; :: thesis:

hence v1 .adj e = v2 by A2, A4, Def41; :: thesis:

end;

suppose v1 <> v2 ; :: thesis:

hence v1 .adj e = v2 by A2, A4, Def41; :: thesis:

end;

end;

end;

hence v1 .adj e = v2 ; :: thesis:
thus v2 .adj e = v1 by A2, A4, Def41; :: thesis:

end;

end;

end;

hence ( v1 .adj e = v2 & v2 .adj e = v1 ) ; :: thesis: