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;

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

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

hence ( u is simplicial iff v is simplicial ) by A4; :: thesis: verum

end;

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

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

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;

set Ha = the AdjGraph of G2,{v};
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

proof

assume G .AdjacentSet {u} <> {} ; :: according to CHORD:def 7 :: thesis: for G2 being AdjGraph of G,{u} holds G2 is complete
let Ga be AdjGraph of G,{u}; :: thesis: Ga is complete
Ga == the AdjGraph of G2,{v} by A1, A2, A3, A5, Th59;
hence Ga is complete by A8, Th61; :: thesis: verum

end;

end;

end;