let G be _Graph; :: thesis: for v being Vertex of G st 3 c= G .order() & v is endvertex holds
ex u, w being Vertex of G st
( u <> v & w <> v & u <> w & u,v are_adjacent & not v,w are_adjacent )
let v be Vertex of G; :: thesis: ( 3 c= G .order() & v is endvertex implies ex u, w being Vertex of G st
( u <> v & w <> v & u <> w & u,v are_adjacent & not v,w are_adjacent ) )
assume A1: ( 3 c= G .order() & v is endvertex ) ; :: thesis: ex u, w being Vertex of G st
( u <> v & w <> v & u <> w & u,v are_adjacent & not v,w are_adjacent )
then A2: 3 c= card (the_Vertices_of G) ;
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 u being Vertex of G such that
A4: e Joins v,u,G by GLIB_000:64;
consider w being object such that
A5: ( w in the_Vertices_of G & w <> v & w <> u ) by A2, PENCIL_1:6;
reconsider w = w as Vertex of G by A5;
take u ; :: thesis: ex w being Vertex of G st
( u <> v & w <> v & u <> w & u,v are_adjacent & not v,w are_adjacent )
take w ; :: thesis: ( u <> v & w <> v & u <> w & u,v are_adjacent & not v,w are_adjacent )
thus ( u <> v & w <> v & u <> w ) by A3, A4, A5; :: thesis: ( u,v are_adjacent & not v,w are_adjacent )
thus u,v are_adjacent by A4, CHORD:def 3; :: thesis: not v,w are_adjacent
hence not v,w are_adjacent by A1, A5, Th100; :: thesis: verum