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 ;
suppose G .AdjacentSet {v} = {} ; :: thesis: contradiction
end;
suppose A3: G .AdjacentSet {v} <> {} ; :: thesis: contradiction
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;
A8: aa,vv are_adjacent by ;
A9: bb,vv are_adjacent by ;
aa <> vv by ;
then aa,bb are_adjacent by A2, A5, A8, A9;
hence a,b are_adjacent by A3, A4, Th44; :: thesis: verum
end;
hence H is complete ; :: thesis: verum
end;
hence contradiction by A1; :: thesis: verum
end;
end;