let G be _Graph; :: thesis: for S being non empty Subset of (the_Vertices_of G)

for H being inducedSubgraph of G,S

for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds

for v being Vertex of H st u = v holds

( u is simplicial iff v is simplicial )

let S be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,S

for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds

for v being Vertex of H st u = v holds

( u is simplicial iff v is simplicial )

let G2 be inducedSubgraph of G,S; :: thesis: for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds

for v being Vertex of G2 st u = v holds

( u is simplicial iff v is simplicial )

let u be Vertex of G; :: thesis: ( u in S & G .AdjacentSet {u} c= S implies for v being Vertex of G2 st u = v holds

( u is simplicial iff v is simplicial ) )

assume that

A1: u in S and

A2: G .AdjacentSet {u} c= S ; :: thesis: for v being Vertex of G2 st u = v holds

( u is simplicial iff v is simplicial )

let v be Vertex of G2; :: thesis: ( u = v implies ( u is simplicial iff v is simplicial ) )

assume A3: u = v ; :: thesis: ( u is simplicial iff v is simplicial )

A4: ( G .AdjacentSet {u} = {} iff G2 .AdjacentSet {v} = {} ) by A1, A2, A3, Th57;

for H being inducedSubgraph of G,S

for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds

for v being Vertex of H st u = v holds

( u is simplicial iff v is simplicial )

let S be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,S

for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds

for v being Vertex of H st u = v holds

( u is simplicial iff v is simplicial )

let G2 be inducedSubgraph of G,S; :: thesis: for u being Vertex of G st u in S & G .AdjacentSet {u} c= S holds

for v being Vertex of G2 st u = v holds

( u is simplicial iff v is simplicial )

let u be Vertex of G; :: thesis: ( u in S & G .AdjacentSet {u} c= S implies for v being Vertex of G2 st u = v holds

( u is simplicial iff v is simplicial ) )

assume that

A1: u in S and

A2: G .AdjacentSet {u} c= S ; :: thesis: for v being Vertex of G2 st u = v holds

( u is simplicial iff v is simplicial )

let v be Vertex of G2; :: thesis: ( u = v implies ( u is simplicial iff v is simplicial ) )

assume A3: u = v ; :: thesis: ( u is simplicial iff v is simplicial )

A4: ( G .AdjacentSet {u} = {} iff G2 .AdjacentSet {v} = {} ) by A1, A2, A3, Th57;

per cases
( G .AdjacentSet {u} = {} or G .AdjacentSet {u} <> {} )
;

end;

suppose A5:
G .AdjacentSet {u} <> {}
; :: thesis: ( u is simplicial iff v is simplicial )

assume A7: v is simplicial ; :: thesis: u is simplicial

G2 .AdjacentSet {v} <> {} by A1, A2, A3, A5, Th57;

then A8: the AdjGraph of G2,{v} is complete by A7;

thus u is simplicial :: thesis: verumend;

hereby :: thesis: ( v is simplicial implies u is simplicial )

set Ha = the AdjGraph of G2,{v};set Ga = the AdjGraph of G,{u};

assume u is simplicial ; :: thesis: v is simplicial

then A6: the AdjGraph of G,{u} is complete by A5;

thus v is simplicial by A1, A2, A3, A5, A6, Th59, Th61; :: thesis: verum

end;assume u is simplicial ; :: thesis: v is simplicial

then A6: the AdjGraph of G,{u} is complete by A5;

thus v is simplicial by A1, A2, A3, A5, A6, Th59, Th61; :: thesis: verum

assume A7: v is simplicial ; :: thesis: u is simplicial

G2 .AdjacentSet {v} <> {} by A1, A2, A3, A5, Th57;

then A8: the AdjGraph of G2,{v} is complete by A7;

thus u is simplicial :: thesis: verum