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