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,() by Def5;
then reconsider u = a as Vertex of the AdjGraph of G,{x} by ;
reconsider v = b as Vertex of the AdjGraph of G,{x} by ;
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 ;
hence ex e being object st e Joins a,b,G ; :: thesis: verum