set X = { (card A) where A is independent Subset of M : A c= C } ;
defpred S1[ Nat] means ex A being independent Subset of M st
( A c= C & $1 = card A );
defpred S2[ Nat] means for A being independent Subset of M st A c= C holds
card A <= $1;
consider n being Nat such that
A1: for A being finite Subset of M st A is independent holds
card A <= n by Def6;
A2: ex ne being Nat st S2[ne]
proof
take n ; :: thesis: S2[n]
thus S2[n] by A1; :: thesis: verum
end;
consider n0 being Nat such that
A3: ( S2[n0] & ( for m being Nat st S2[m] holds
n0 <= m ) ) from NAT_1:sch 5(A2);
 union { (card A) where A is independent Subset of M : A c= C } = n0
proof
now :: thesis: for a being set st a in { (card A) where A is independent Subset of M : A c= C } holds
a c= Segm n0
let a be set ; :: thesis: ( a in { (card A) where A is independent Subset of M : A c= C } implies a c= Segm n0 )
assume a in { (card A) where A is independent Subset of M : A c= C } ; :: thesis: a c= Segm n0
then consider A being independent Subset of M such that
A4: a = card A and
A5: A c= C ;
card A <= n0 by A3, A5;
then Segm (card A) c= Segm n0 by NAT_1:39;
hence a c= Segm n0 by A4; :: thesis: verum
end;
hence union { (card A) where A is independent Subset of M : A c= C } c= n0 by ZFMISC_1:76; :: according to XBOOLE_0:def 10 :: thesis: not n0 c/= union { (card A) where A is independent Subset of M : A c= C }
A6: {} M c= C ;
A7: for k being Nat st S1[k] holds
k <= n0 by A3;
card {} = card {} ;
then A8: ex n being Nat st S1[n] by A6;
consider n being Nat such that
A9: ( S1[n] & ( for m being Nat st S1[m] holds
m <= n ) ) from NAT_1:sch 6(A7, A8);
 S2[n] by A9;
then A10: n0 <= n by A3;
n <= n0 by A3, A9;
then n = n0 by A10, XXREAL_0:1;
then n0 in { (card A) where A is independent Subset of M : A c= C } by A9;
hence not n0 c/= union { (card A) where A is independent Subset of M : A c= C } by ZFMISC_1:74; :: thesis: verum
end;
hence union { (card A) where A is independent Subset of M : A c= C } is Nat ; :: thesis: verum