let G be finite chordal _Graph; :: thesis: ex v being Vertex of G st v is simplicial

per cases ( G is complete or not G is complete ) ;

suppose A1: G is complete ; :: thesis: ex v being Vertex of G st v is simplicial

consider u being Vertex of G;
u is simplicial by A1, Th64;
hence ex v being Vertex of G st v is simplicial ; :: thesis: verum

end;

suppose A2: not G is complete ; :: thesis: ex v being Vertex of G st v is simplicial

then not G is trivial ;
then consider a, b being Vertex of G such that
A3: ( a <> b & not a,b are_adjacent & a is simplicial & b is simplicial ) by A2, Th102;
thus ex v being Vertex of G st v is simplicial by A3; :: thesis: verum

end;

end;