let G be finite trivial _Graph; :: thesis: for v being Vertex of G ex S being VertexScheme of G st
( S = <*v*> & S is perfect )

let v be Vertex of G; :: thesis: ex S being VertexScheme of G st
( S = <*v*> & S is perfect )

consider v1 being Vertex of G such that
A1: the_Vertices_of G = {v1} by GLIB_000:22;
set S = <*v*>;
v1 = v by ;
then A2: rng <*v*> = the_Vertices_of G by ;
<*v*> is one-to-one by FINSEQ_3:93;
then reconsider S = <*v*> as VertexScheme of G by ;
take S ; :: thesis: ( S = <*v*> & S is perfect )
thus S = <*v*> ; :: thesis: S is perfect
let n be non zero Nat; :: according to CHORD:def 13 :: thesis: ( n <= len S implies for Gf being inducedSubgraph of G,()
for v being Vertex of Gf st v = S . n holds
v is simplicial )

assume n <= len S ; :: thesis: for Gf being inducedSubgraph of G,()
for v being Vertex of Gf st v = S . n holds
v is simplicial

let Gf be inducedSubgraph of G,(); :: thesis: for v being Vertex of Gf st v = S . n holds
v is simplicial

thus for v being Vertex of Gf st v = S . n holds
v is simplicial ; :: thesis: verum