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 :: thesis: for p being set st p in D holds
(G SubgraphInducedBy S) SubgraphInducedBy p is Clique of (G SubgraphInducedBy S)

let p be set ; :: thesis: ( p in D implies (G SubgraphInducedBy S) SubgraphInducedBy p is Clique of (G SubgraphInducedBy S) )
assume A2: p in D ; :: thesis: (G SubgraphInducedBy S) SubgraphInducedBy p is Clique of (G SubgraphInducedBy S)
set Hp = (G SubgraphInducedBy S) SubgraphInducedBy p;

now :: thesis: 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 p

let x, y be set ; :: thesis: ( 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) ; :: thesis: {x,y} in (G SubgraphInducedBy S) SubgraphInducedBy p
consider 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; :: thesis: 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) ; :: thesis: verum

end;

then reconsider D = D as Clique-partition of (G SubgraphInducedBy S) by Def16;
take D ; :: according to SCMYCIEL:def 17 :: thesis: D is finite
thus D is finite by A1; :: thesis: verum