let G be _Graph; for v1, v2 being Vertex of G
for e being object st e Joins v1,v2,G holds
( v1 .adj e = v2 & v2 .adj e = v1 )
let v1, v2 be Vertex of G; for e being object st e Joins v1,v2,G holds
( v1 .adj e = v2 & v2 .adj e = v1 )
let e be object ; ( e Joins v1,v2,G implies ( v1 .adj e = v2 & v2 .adj e = v1 ) )
assume A1:
e Joins v1,v2,G
; ( v1 .adj e = v2 & v2 .adj e = v1 )
then A2:
e in v1 .edgesInOut()
by Th62;
hence
( v1 .adj e = v2 & v2 .adj e = v1 )
; verum