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 :: thesis: for G2 being AdjGraph of G,{v} holds G2 is complete

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 Th62; :: thesis: verum

end;

hence v is simplicial ; :: thesis: verum