let G be _Graph; :: thesis: for v being Vertex of G st v is simplicial holds

for a, b being object st a <> b & a in G .AdjacentSet {v} & b in G .AdjacentSet {v} holds

ex e being object st e Joins a,b,G

let x be Vertex of G; :: thesis: ( x is simplicial implies for a, b being object st a <> b & a in G .AdjacentSet {x} & b in G .AdjacentSet {x} holds

ex e being object st e Joins a,b,G )

assume A1: x is simplicial ; :: thesis: for a, b being object st a <> b & a in G .AdjacentSet {x} & b in G .AdjacentSet {x} holds

ex e being object st e Joins a,b,G

set H = the AdjGraph of G,{x};

let a, b be object ; :: thesis: ( a <> b & a in G .AdjacentSet {x} & b in G .AdjacentSet {x} implies ex e being object st e Joins a,b,G )

assume that

A2: a <> b and

A3: a in G .AdjacentSet {x} and

A4: b in G .AdjacentSet {x} ; :: thesis: ex e being object st e Joins a,b,G

A5: the AdjGraph of G,{x} is inducedSubgraph of G,(G .AdjacentSet {x}) by Def5;

then reconsider u = a as Vertex of the AdjGraph of G,{x} by A3, GLIB_000:def 37;

reconsider v = b as Vertex of the AdjGraph of G,{x} by A4, A5, GLIB_000:def 37;

the AdjGraph of G,{x} is complete by A1, A3;

then u,v are_adjacent by A2;

then consider e being object such that

A6: e Joins u,v, the AdjGraph of G,{x} ;

e Joins a,b,G by A6, GLIB_000:72;

hence ex e being object st e Joins a,b,G ; :: thesis: verum

for a, b being object st a <> b & a in G .AdjacentSet {v} & b in G .AdjacentSet {v} holds

ex e being object st e Joins a,b,G

let x be Vertex of G; :: thesis: ( x is simplicial implies for a, b being object st a <> b & a in G .AdjacentSet {x} & b in G .AdjacentSet {x} holds

ex e being object st e Joins a,b,G )

assume A1: x is simplicial ; :: thesis: for a, b being object st a <> b & a in G .AdjacentSet {x} & b in G .AdjacentSet {x} holds

ex e being object st e Joins a,b,G

set H = the AdjGraph of G,{x};

let a, b be object ; :: thesis: ( a <> b & a in G .AdjacentSet {x} & b in G .AdjacentSet {x} implies ex e being object st e Joins a,b,G )

assume that

A2: a <> b and

A3: a in G .AdjacentSet {x} and

A4: b in G .AdjacentSet {x} ; :: thesis: ex e being object st e Joins a,b,G

A5: the AdjGraph of G,{x} is inducedSubgraph of G,(G .AdjacentSet {x}) by Def5;

then reconsider u = a as Vertex of the AdjGraph of G,{x} by A3, GLIB_000:def 37;

reconsider v = b as Vertex of the AdjGraph of G,{x} by A4, A5, GLIB_000:def 37;

the AdjGraph of G,{x} is complete by A1, A3;

then u,v are_adjacent by A2;

then consider e being object such that

A6: e Joins u,v, the AdjGraph of G,{x} ;

e Joins a,b,G by A6, GLIB_000:72;

hence ex e being object st e Joins a,b,G ; :: thesis: verum