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 A1: ( u in S & 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 A2: u = v ; :: thesis: ( u is simplicial iff v is simplicial )
A3: ( G .AdjacentSet {u} = {} iff G2 .AdjacentSet {v} = {} ) by A1, A2, Th58;

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 A3, Def7; :: thesis: verum

end;

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

then A5: G2 .AdjacentSet {v} <> {} by A1, A2, Th58;

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

assume A6: u is simplicial ; :: thesis: v is simplicial
consider Ga being AdjGraph of G,{u};
A7: Ga is complete by A4, A6, Def7;
thus v is simplicial :: thesis: verum

proof

assume G2 .AdjacentSet {v} <> {} ; :: according to CHORD:def 7 :: thesis: for G2 being AdjGraph of G2,{v} holds G2 is complete
let Ha be AdjGraph of G2,{v}; :: thesis: Ha is complete
thus Ha is complete by A1, A2, A4, A7, Th60, Th62; :: thesis: verum

end;

end;

assume A8: v is simplicial ; :: thesis: u is simplicial
consider Ha being AdjGraph of G2,{v};
A9: Ha is complete by A5, A8, Def7;
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 == Ha by A1, A2, A4, Th60;
hence Ga is complete by A9, Th62; :: thesis: verum

end;

end;

end;