let G be complete _Graph; :: thesis: for v being Vertex of holds v is simplicial
let v be Vertex of ; :: thesis: v is simplicial

now

let G2 be AdjGraph of G,{v}; :: thesis: G2 is complete
G2 is inducedSubgraph of G,{v} by Def5;
hence G2 is complete by Th63; :: thesis: verum

end;

hence v is simplicial by Def7; :: thesis: verum