let it1, it2 be Nat; ( ex A being finite StableSet of R st card A = it1 & ( for T being finite StableSet of R holds card T <= it1 ) & ex A being finite StableSet of R st card A = it2 & ( for T being finite StableSet of R holds card T <= it2 ) implies it1 = it2 )
assume that
Aa:
ex S1 being finite StableSet of R st card S1 = it1
and
A1:
for T being finite StableSet of R holds card T <= it1
and
Ab:
ex S2 being finite StableSet of R st card S2 = it2
and
A2:
for T being finite StableSet of R holds card T <= it2
; it1 = it2
consider S1 being finite StableSet of R such that
A3:
card S1 = it1
by Aa;
consider S2 being finite StableSet of R such that
A4:
card S2 = it2
by Ab;
( it1 <= it2 & it2 <= it1 )
by A1, A2, A3, A4;
hence
it1 = it2
by XXREAL_0:1; verum