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