let G be _Graph; :: thesis: for v being Vertex of G st not v is simplicial holds
ex a, b being Vertex of G st
( a <> b & v <> a & v <> b & v,a are_adjacent & v,b are_adjacent & not a,b are_adjacent )

let v be Vertex of G; :: thesis: ( not v is simplicial implies ex a, b being Vertex of G st
( a <> b & v <> a & v <> b & v,a are_adjacent & v,b are_adjacent & not a,b are_adjacent ) )

assume A1: not v is simplicial ; :: thesis: ex a, b being Vertex of G st
( a <> b & v <> a & v <> b & v,a are_adjacent & v,b are_adjacent & not a,b are_adjacent )

assume A2: for a, b being Vertex of G holds
( not a <> b or not v <> a or not v <> b or not v,a are_adjacent or not v,b are_adjacent or a,b are_adjacent ) ; :: thesis: contradiction
per cases ;
end;
now :: thesis: for H being AdjGraph of G,{v} holds H is complete
let H be AdjGraph of G,{v}; :: thesis: H is complete
A4: H is inducedSubgraph of G,() by Def5;
now :: thesis: for a, b being Vertex of H st a <> b holds
let a, b be Vertex of H; :: thesis: ( a <> b implies a,b are_adjacent )
assume A5: a <> b ; :: thesis: a,b are_adjacent
A6: the_Vertices_of H = G .AdjacentSet {v} by ;
then A7: b in G .AdjacentSet {v} ;
a in G .AdjacentSet {v} by A6;
then reconsider vv = v, aa = a, bb = b as Vertex of G by A7;