let G be _Graph; :: thesis: for e, x, y being set
for v being Vertex of G st e in v .edgesInOut() & e Joins x,y,G & not v = x holds
v = y
let e, x, y be set ; :: thesis: for v being Vertex of G st e in v .edgesInOut() & e Joins x,y,G & not v = x holds
v = y
let v be Vertex of G; :: thesis: ( e in v .edgesInOut() & e Joins x,y,G & not v = x implies v = y )
assume that
A1: e in v .edgesInOut() and
A2: e Joins x,y,G ; :: thesis: ( v = x or v = y )

now

assume A3: v <> x ; :: thesis: v = y

now

per cases ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) by A1, Th64;

suppose (the_Source_of G) . e = v ; :: thesis: v = y

hence v = y by A2, A3, Def15; :: thesis: verum

end;

suppose (the_Target_of G) . e = v ; :: thesis: v = y

hence v = y by A2, A3, Def15; :: thesis: verum

end;

end;

end;

hence v = y ; :: thesis: verum

end;

hence ( v = x or v = y ) ; :: thesis: verum