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

set u = the Vertex of G;
the Vertex of G is simplicial by A1, Th63;
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 ex a, b being Vertex of G st
( a <> b & not a,b are_adjacent & a is simplicial & b is simplicial ) by A2, Th101;
hence ex v being Vertex of G st v is simplicial ; :: thesis: verum

end;

end;