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
A2:
ex S1 being finite StableSet of R st card S1 = it1
and
A3:
for T being finite StableSet of R holds card T <= it1
and
A4:
ex S2 being finite StableSet of R st card S2 = it2
and
A5:
for T being finite StableSet of R holds card T <= it2
; it1 = it2
consider S1 being finite StableSet of R such that
A6:
card S1 = it1
by A2;
consider S2 being finite StableSet of R such that
A7:
card S2 = it2
by A4;
( it1 <= it2 & it2 <= it1 )
by A3, A5, A6, A7;
hence
it1 = it2
by XXREAL_0:1; verum