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

let v be Vertex of G; :: thesis: v is simplicial

now :: thesis: for G2 being AdjGraph of G,{v} holds G2 is complete

hence
v is simplicial
; :: thesis: verumlet 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;G2 is inducedSubgraph of G,(G .AdjacentSet {v}) by Def5;

hence G2 is complete by Th62; :: thesis: verum