let it1, it2 be Nat; ( ex C being finite Clique-partition of G st card C = it1 & ( for C being finite Clique-partition of G holds it1 <= card C ) & ex C being finite Clique-partition of G st card C = it2 & ( for C being finite Clique-partition of G holds it2 <= card C ) implies it1 = it2 )
assume that
A1:
ex C being finite Clique-partition of G st card C = it1
and
A1a:
for C being finite Clique-partition of G holds it1 <= card C
and
A2:
ex C being finite Clique-partition of G st card C = it2
and
A2a:
for C being finite Clique-partition of G holds it2 <= card C
; it1 = it2
consider C1 being finite Clique-partition of G such that
B1:
card C1 = it1
by A1;
consider C2 being finite Clique-partition of G such that
B2:
card C2 = it2
by A2;
( it1 <= card C2 & it2 <= card C1 )
by A1a, A2a;
hence
it1 = it2
by B1, B2, XXREAL_0:1; verum