theorem Th101: :: GLIBPRE0:95

for G being _Graph
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 )