set H = G SubgraphInducedBy S;
consider C being Clique-partition of G such that
A: C is finite by Lwfclicov;
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 A1: 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
B2: x in union ((G SubgraphInducedBy S) SubgraphInducedBy p) and
C2: 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
D2: p = c /\ VH and
c meets VH by A1;
G2: x in p by B2, Sub1;
H2: y in p by C2, Sub1;
I2a: x in VH by D2, G2, XBOOLE_0:def 4;
I2aa: y in VH by D2, H2, XBOOLE_0:def 4;
set Gc = G SubgraphInducedBy c;
I2: G SubgraphInducedBy c is Clique of G by I2a, LCliquewise;
I2b: G SubgraphInducedBy c = CompleteSGraph (Vertices (G SubgraphInducedBy c)) by I2, Lclique;
( x in c & y in c ) by G2, H2, D2, XBOOLE_0:def 4;
then ( x in Vertices (G SubgraphInducedBy c) & y in Vertices (G SubgraphInducedBy c) ) by Sub3;
then F2aa: {x,y} in G SubgraphInducedBy c by I2b, CSG1;
( x in S & y in S ) by I2a, I2aa, Sub1;
then {x,y} c= S by ZFMISC_1:32;
then F2: {x,y} in G SubgraphInducedBy S by F2aa, XBOOLE_0:def 4;
{x,y} c= p by G2, H2, ZFMISC_1:32;
hence {x,y} in (G SubgraphInducedBy S) SubgraphInducedBy p by F2, XBOOLE_0:def 4; :: thesis: verum

end;

then (G SubgraphInducedBy S) SubgraphInducedBy p = CompleteSGraph (Vertices ((G SubgraphInducedBy S) SubgraphInducedBy p)) by CSGdef;
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 LCliquewise;
take D ; :: according to SCMYCIEL:def 17 :: thesis: D is finite
thus D is finite by A; :: thesis: verum