let G be SimpleGraph; :: thesis: ( G is finite implies G is with_finite_cliquecover# )
assume A1: G is finite ; :: thesis: G is with_finite_cliquecover#
set VG = Vertices G;
per cases ( Vertices G is empty or not Vertices G is empty ) ;
suppose Vertices G is empty ; :: thesis: G is with_finite_cliquecover#
then reconsider S = {} as a_partition of Vertices G by EQREL_1:45;
for x being set st x in S holds
G SubgraphInducedBy x is Clique of G ;
then reconsider S = S as Clique-partition of G by Def16;
take S ; :: according to SCMYCIEL:def 17 :: thesis: S is finite
thus S is finite ; :: thesis: verum
end;
suppose A2: not Vertices G is empty ; :: thesis: G is with_finite_cliquecover#
defpred S1[ set ] means verum;
reconsider cRp1 = Vertices G as non empty finite set by A2, A1;
set S = SmallestPartition (Vertices G);
deffunc H1( set ) -> set = {c1};
A3: SmallestPartition (Vertices G) = { H1(x) where x is Element of cRp1 : S1[x] } by EQREL_1:37;
A4: { H1(x) where x is Element of cRp1 : S1[x] } is finite from PRE_CIRC:sch 1();
now :: thesis: for z being set st z in SmallestPartition (Vertices G) holds
G SubgraphInducedBy z is Clique of G
let z be set ; :: thesis: ( z in SmallestPartition (Vertices G) implies G SubgraphInducedBy z is Clique of G )
assume A5: z in SmallestPartition (Vertices G) ; :: thesis: G SubgraphInducedBy z is Clique of G
consider x being Element of Vertices G such that
A6: z = {x} by A5, A3;
G SubgraphInducedBy z = {{},{x}} by A6, A2, Th46;
hence G SubgraphInducedBy z is Clique of G by A2, Th50; :: thesis: verum
end;
then reconsider S = SmallestPartition (Vertices G) as Clique-partition of G by Def16;
take S ; :: according to SCMYCIEL:def 17 :: thesis: S is finite
thus S is finite by A4; :: thesis: verum
end;
end;