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

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} <> {} )
;

end;

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

end;

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

hence
contradiction
by A1; :: thesis: verumlet H be AdjGraph of G,{v}; :: thesis: H is complete

A4: H is inducedSubgraph of G,(G .AdjacentSet {v}) by Def5;

end;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

hence
H is complete
; :: thesis: veruma,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;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