set X = { (card A) where A is independent Subset of M : A c= C } ;

defpred S_{1}[ Nat] means ex A being independent Subset of M st

( A c= C & $1 = card A );

defpred S_{2}[ 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 S_{2}[ne]
consider n0 being Nat such that

A3: ( S_{2}[n0] & ( for m being Nat st S_{2}[m] holds

n0 <= m ) ) from NAT_1:sch 5(A2);

union { (card A) where A is independent Subset of M : A c= C } = n0

defpred S

( A c= C & $1 = card A );

defpred S

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 S

A3: ( S

n0 <= m ) ) from NAT_1:sch 5(A2);

union { (card A) where A is independent Subset of M : A c= C } = n0

proof

A6: {} M c= C ;

A7: for k being Nat st S_{1}[k] holds

k <= n0 by A3;

card {} = card {} ;

then A8: ex n being Nat st S_{1}[n]
by A6;

consider n being Nat such that

A9: ( S_{1}[n] & ( for m being Nat st S_{1}[m] holds

m <= n ) ) from NAT_1:sch 6(A7, A8);

S_{2}[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: verumnow :: 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

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 } 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;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

A6: {} M c= C ;

A7: for k being Nat st S

k <= n0 by A3;

card {} = card {} ;

then A8: ex n being Nat st S

consider n being Nat such that

A9: ( S

m <= n ) ) from NAT_1:sch 6(A7, A8);

S

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