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 A1, TARSKI:def 1;

then A2: rng <*v*> = the_Vertices_of G by A1, FINSEQ_1:39;

<*v*> is one-to-one by FINSEQ_3:93;

then reconsider S = <*v*> as VertexScheme of G by A2, Def12;

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,(S .followSet n)

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,(S .followSet n)

for v being Vertex of Gf st v = S . n holds

v is simplicial

let Gf be inducedSubgraph of G,(S .followSet n); :: 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

( 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 A1, TARSKI:def 1;

then A2: rng <*v*> = the_Vertices_of G by A1, FINSEQ_1:39;

<*v*> is one-to-one by FINSEQ_3:93;

then reconsider S = <*v*> as VertexScheme of G by A2, Def12;

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,(S .followSet n)

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,(S .followSet n)

for v being Vertex of Gf st v = S . n holds

v is simplicial

let Gf be inducedSubgraph of G,(S .followSet n); :: 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