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

now

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

end;

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