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
consider H being AdjGraph of G,{x};
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 that
A2: a <> b and
A3: a in G .AdjacentSet {x} and
A4: b in G .AdjacentSet {x} ; :: thesis: ex e being set st e Joins a,b,G
A5: H is inducedSubgraph of G,(G .AdjacentSet {x}) by Def5;
then reconsider u = a as Vertex of H by A3, GLIB_000:def 39;
reconsider v = b as Vertex of H by A4, A5, GLIB_000:def 39;
H is complete by A1, A3, Def7;
then u,v are_adjacent by A2, Def6;
then consider e being set such that
A6: e Joins u,v,H by Def3;
e Joins a,b,G by A6, GLIB_000:75;
hence ex e being set st e Joins a,b,G ; :: thesis: verum