let G be finite chordal _Graph; :: thesis: ex v being Vertex of 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 st v is simplicial

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

end;

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

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

end;

end;