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

end;

suppose A3: G .AdjacentSet {v} <> {} ; :: thesis: contradiction

now

let H be AdjGraph of G,{v}; :: thesis: H is complete
A4: H is inducedSubgraph of G,(G .AdjacentSet {v}) by Def5;

now

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 39;
then ( a in G .AdjacentSet {v} & b in G .AdjacentSet {v} ) ;
then reconsider vv = v, aa = a, bb = b as Vertex of G ;
A7: ( aa <> vv & aa,vv are_adjacent ) by A6, Th52;
( bb <> vv & bb,vv are_adjacent ) by A6, Th52;
then aa,bb are_adjacent by A2, A5, A7;
hence a,b are_adjacent by A3, A4, Th45; :: thesis: verum

end;

hence H is complete by Def6; :: thesis: verum

end;

hence contradiction by A1, Def7; :: thesis: verum

end;

end;