let it1, it2 be Nat; ( ex C being finite Clique of R st card C = it1 & ( for T being finite Clique of R holds card T <= it1 ) & ex C being finite Clique of R st card C = it2 & ( for T being finite Clique of R holds card T <= it2 ) implies it1 = it2 )
assume that
A1a:
ex S1 being finite Clique of R st card S1 = it1
and
A1b:
for T being finite Clique of R holds card T <= it1
and
A2a:
ex S2 being finite Clique of R st card S2 = it2
and
A2b:
for T being finite Clique of R holds card T <= it2
; it1 = it2
consider S1 being finite Clique of R such that
A1:
card S1 = it1
by A1a;
consider S2 being finite Clique of R such that
A2:
card S2 = it2
by A2a;
( it1 <= it2 & it2 <= it1 )
by A1, A2, A1b, A2b;
hence
it1 = it2
by XXREAL_0:1; verum