let G be _Graph; :: thesis: for S being non empty Subset of ()
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 (); :: 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 ;
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 ) 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 ; :: thesis: verum
end;
end;
end;