set H = G SubgraphInducedBy S;
consider C being Clique-partition of G such that
A1:
C is finite
by Def17;
reconsider VH = Vertices (G SubgraphInducedBy S) as Subset of (Vertices G) by ZFMISC_1:77;
reconsider D = C | VH as a_partition of Vertices (G SubgraphInducedBy S) ;
now for p being set st p in D holds
(G SubgraphInducedBy S) SubgraphInducedBy p is Clique of (G SubgraphInducedBy S)let p be
set ;
( p in D implies (G SubgraphInducedBy S) SubgraphInducedBy p is Clique of (G SubgraphInducedBy S) )assume A2:
p in D
;
(G SubgraphInducedBy S) SubgraphInducedBy p is Clique of (G SubgraphInducedBy S)set Hp =
(G SubgraphInducedBy S) SubgraphInducedBy p;
now for x, y being set st x in union ((G SubgraphInducedBy S) SubgraphInducedBy p) & y in union ((G SubgraphInducedBy S) SubgraphInducedBy p) holds
{x,y} in (G SubgraphInducedBy S) SubgraphInducedBy plet x,
y be
set ;
( x in union ((G SubgraphInducedBy S) SubgraphInducedBy p) & y in union ((G SubgraphInducedBy S) SubgraphInducedBy p) implies {x,y} in (G SubgraphInducedBy S) SubgraphInducedBy p )assume that A3:
x in union ((G SubgraphInducedBy S) SubgraphInducedBy p)
and A4:
y in union ((G SubgraphInducedBy S) SubgraphInducedBy p)
;
{x,y} in (G SubgraphInducedBy S) SubgraphInducedBy pconsider c being
Element of
C such that A5:
p = c /\ VH
and
c meets VH
by A2;
A6:
x in p
by A3, Lm7;
A7:
y in p
by A4, Lm7;
A8:
x in VH
by A5, A6, XBOOLE_0:def 4;
A9:
y in VH
by A5, A7, XBOOLE_0:def 4;
set Gc =
G SubgraphInducedBy c;
A10:
G SubgraphInducedBy c is
Clique of
G
by A8, Def16;
A11:
G SubgraphInducedBy c = CompleteSGraph (Vertices (G SubgraphInducedBy c))
by A10, Def13;
(
x in c &
y in c )
by A6, A7, A5, XBOOLE_0:def 4;
then
(
x in Vertices (G SubgraphInducedBy c) &
y in Vertices (G SubgraphInducedBy c) )
by Lm8;
then A12:
{x,y} in G SubgraphInducedBy c
by A11, Th34;
(
x in S &
y in S )
by A8, A9, Lm7;
then
{x,y} c= S
by ZFMISC_1:32;
then A13:
{x,y} in G SubgraphInducedBy S
by A12, XBOOLE_0:def 4;
{x,y} c= p
by A6, A7, ZFMISC_1:32;
hence
{x,y} in (G SubgraphInducedBy S) SubgraphInducedBy p
by A13, XBOOLE_0:def 4;
verum end; then
(G SubgraphInducedBy S) SubgraphInducedBy p = CompleteSGraph (Vertices ((G SubgraphInducedBy S) SubgraphInducedBy p))
by Th32;
hence
(G SubgraphInducedBy S) SubgraphInducedBy p is
Clique of
(G SubgraphInducedBy S)
;
verum end;
then reconsider D = D as Clique-partition of (G SubgraphInducedBy S) by Def16;
take
D
; SCMYCIEL:def 17 D is finite
thus
D is finite
by A1; verum