let G be _Graph; :: thesis: for v being Vertex of G st v is simplicial holds
for a, b being set st a <> b & a in G .AdjacentSet {v} & b in G .AdjacentSet {v} holds
ex e being set st e Joins a,b,G
let x be Vertex of G; :: thesis: ( x is simplicial implies for a, b being set st a <> b & a in G .AdjacentSet {x} & b in G .AdjacentSet {x} holds
ex e being set st e Joins a,b,G )
assume A1: x is simplicial ; :: thesis: for a, b being set st a <> b & a in G .AdjacentSet {x} & b in G .AdjacentSet {x} holds
ex e being set st e Joins a,b,G
let a, b be set ; :: thesis: ( a <> b & a in G .AdjacentSet {x} & b in G .AdjacentSet {x} implies ex e being set st e Joins a,b,G )
assume A2: ( a <> b & a in G .AdjacentSet {x} & b in G .AdjacentSet {x} ) ; :: thesis: ex e being set st e Joins a,b,G
consider H being AdjGraph of G,{x};
A3: H is complete by A1, A2, Def7;
A4: H is inducedSubgraph of G,(G .AdjacentSet {x}) by Def5;
then reconsider u = a as Vertex of H by A2, GLIB_000:def 39;
reconsider v = b as Vertex of H by A2, A4, GLIB_000:def 39;
u,v are_adjacent by A2, A3, Def6;
then consider e being set such that
A5: e Joins u,v,H by Def3;
e Joins a,b,G by A5, GLIB_000:75;
hence ex e being set st e Joins a,b,G ; :: thesis: verum