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 )
;

end;

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;the Vertex of G is simplicial by A1, Th63;

hence ex v being Vertex of G st v is simplicial ; :: thesis: verum

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;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