let G be _Graph; :: thesis: for e, x being set
for v1 being Vertex of G st e Joins v1,x,G holds
e in v1 .edgesInOut()
let e, x be set ; :: thesis: for v1 being Vertex of G st e Joins v1,x,G holds
e in v1 .edgesInOut()
let v1 be Vertex of G; :: thesis: ( e Joins v1,x,G implies e in v1 .edgesInOut() )
assume e Joins v1,x,G ; :: thesis: e in v1 .edgesInOut()
then ( e in the_Edges_of G & ( ( (the_Source_of G) . e = v1 & (the_Target_of G) . e = x ) or ( (the_Source_of G) . e = x & (the_Target_of G) . e = v1 ) ) ) by Def15;
hence e in v1 .edgesInOut() by Th64; :: thesis: verum