let G be _Graph; :: thesis: for u, v, w being Vertex of G st v is endvertex & u <> w & u,v are_adjacent holds
not v,w are_adjacent
let u, v, w be Vertex of G; :: thesis: ( v is endvertex & u <> w & u,v are_adjacent implies not v,w are_adjacent )
assume A1: ( v is endvertex & u <> w ) ; :: thesis: ( not u,v are_adjacent or not v,w are_adjacent )
assume A2: u,v are_adjacent ; :: thesis: not v,w are_adjacent
consider e being object such that
A3: ( v .edgesInOut() = {e} & not e Joins v,v,G ) by A1, GLIB_000:def 51;
e in v .edgesInOut() by A3, TARSKI:def 1;
then consider v9 being Vertex of G such that
A4: e Joins v,v9,G by GLIB_000:64;
consider e8 being object such that
A5: e8 Joins v,u,G by A2, CHORD:def 3;
e8 is set by TARSKI:1;
then e8 in v .edgesInOut() by A5, GLIB_000:64;
then e8 = e by A3, TARSKI:def 1;
then A6: ( ( v = v & v9 = u ) or ( v = u & v9 = v ) ) by A4, A5, GLIB_000:15;
for e9 being object holds not e9 Joins v,w,G

proof

given e9 being object such that A7: e9 Joins v,w,G ; :: thesis: contradiction
e9 is set by TARSKI:1;
then e9 in v .edgesInOut() by A7, GLIB_000:64;
then e9 = e by A3, TARSKI:def 1;
then ( ( v = v & w = v9 ) or ( v = v9 & w = v ) ) by A4, A7, GLIB_000:15;
hence contradiction by A1, A6; :: thesis: verum

end;

hence not v,w are_adjacent by CHORD:def 3; :: thesis: verum