let it1, it2 be Nat; ( ex C being finite Coloring of R st card C = it1 & ( for C being finite Coloring of R holds it1 <= card C ) & ex C being finite Coloring of R st card C = it2 & ( for C being finite Coloring of R holds it2 <= card C ) implies it1 = it2 )
assume that
A5:
ex C being finite Coloring of R st card C = it1
and
A6:
for C being finite Coloring of R holds it1 <= card C
and
A7:
ex C being finite Coloring of R st card C = it2
and
A8:
for C being finite Coloring of R holds it2 <= card C
; it1 = it2
consider C1 being finite Coloring of R such that
A9:
card C1 = it1
by A5;
consider C2 being finite Coloring of R such that
A10:
card C2 = it2
by A7;
( it1 <= card C2 & it2 <= card C1 )
by A6, A8;
hence
it1 = it2
by A9, A10, XXREAL_0:1; verum