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