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 ( G .AdjacentSet {v} = {} or G .AdjacentSet {v} <> {} ) ;

suppose G .AdjacentSet {v} = {} ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

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,(G .AdjacentSet {v}) by Def5;

now :: thesis: for a, b being Vertex of H st a <> b holds
a,b are_adjacent

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 A3, A4, GLIB_000:def 37;
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 A6, Th51;
A9: bb,vv are_adjacent by A6, Th51;
aa <> vv by A6, Th51;
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;