let A be Subset-Family of REAL ; :: thesis: ( card A in continuum implies card { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } in continuum )
assume A1: card A in continuum ; :: thesis: card { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } in continuum
set X = { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } ;
set Y = { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } ;
deffunc H₁( set ) -> set = { x where x is Element of REAL : x is_local_minimum_of $1 } ;
A2: for a being set st a in A holds
H₁(a) in bool REAL

proof

let a be set ; :: thesis: ( a in A implies H₁(a) in bool REAL )
H₁(a) c= REAL

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in H₁(a) or b in REAL )
assume b in H₁(a) ; :: thesis: b in REAL
then ex x being Element of REAL st
( b = x & x is_local_minimum_of a ) ;
hence b in REAL ; :: thesis: verum

end;

hence ( a in A implies H₁(a) in bool REAL ) ; :: thesis: verum

end;

consider f being Function of A,(bool REAL ) such that
A3: for a being set st a in A holds
f . a = H₁(a) from FUNCT_2:sch 2(A2);
A4: { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } c= Union f

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } or a in Union f )
assume a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } ; :: thesis: a in Union f
then consider x being Element of REAL such that
A5: ( a = x & ex U being set st
( U in A & x is_local_minimum_of U ) ) ;
consider U being set such that
A6: ( U in A & x is_local_minimum_of U ) by A5;
( a in H₁(U) & f . U = H₁(U) & dom f = A ) by A3, A5, A6, FUNCT_2:def 1;
hence a in Union f by A6, CARD_5:10; :: thesis: verum

end;

{ x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } c= { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } or a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } )
assume a in { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } ; :: thesis: a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) }
then consider x being Element of REAL such that
A7: ( a = x & ex U being set st
( U in UniCl A & x is_local_minimum_of U ) ) ;
consider U being set such that
A8: ( U in UniCl A & x is_local_minimum_of U ) by A7;
reconsider U = U as Subset of REAL by A8;
A9: x in U by A8, Def3;
consider y being real number such that
A10: ( y < x & ].y,x.[ misses U ) by A8, Def3;
consider B being Subset-Family of REAL such that
A11: ( B c= A & U = union B ) by A8, CANTOR_1:def 1;
consider C being set such that
A12: ( x in C & C in B ) by A9, A11, TARSKI:def 4;
reconsider C = C as Subset of REAL by A12;
].y,x.[ misses C

proof

assume not ].y,x.[ misses C ; :: thesis: contradiction
then consider b being set such that
A13: ( b in ].y,x.[ & b in C ) by XBOOLE_0:3;
b in U by A11, A12, A13, TARSKI:def 4;
hence contradiction by A10, A13, XBOOLE_0:3; :: thesis: verum

end;

then ( C in A & x is_local_minimum_of C ) by A10, A11, A12, Def3;
hence a in { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } by A7; :: thesis: verum

end;

then { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } c= Union f by A4, XBOOLE_1:1;
then A14: card { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } c= card (Union f) by CARD_1:27;
A15: for a being set st a in A holds
card (f . a) c= omega

proof

let a be set ; :: thesis: ( a in A implies card (f . a) c= omega )
assume A16: a in A ; :: thesis: card (f . a) c= omega
then reconsider b = a as Subset of REAL ;
f . a = H₁(b) by A3, A16;
then f . a is countable by Th19;
hence card (f . a) c= omega by CARD_3:def 15; :: thesis: verum

end;

A17: now

per cases ( card A is empty or ( not card A is empty & card A is finite ) or not card A is finite ) ;

suppose card A is empty ; :: thesis: (card A) *` omega in continuum

then (card A) *` omega = 0 by CARD_2:32;
hence (card A) *` omega in continuum by ORDINAL3:10; :: thesis: verum

end;

suppose ( not card A is empty & card A is finite ) ; :: thesis: (card A) *` omega in continuum

then ( 0 in card A & card (card A) in omega & card (card A) = card A ) by CARD_3:101, ORDINAL3:10;
hence (card A) *` omega in continuum by Th30, CARD_4:78; :: thesis: verum

end;

suppose A18: not card A is finite ; :: thesis: (card A) *` omega in continuum

then ( 0 in omega & omega c= card A ) by CARD_5:25;
hence (card A) *` omega in continuum by A1, A18, CARD_4:78; :: thesis: verum

end;

end;

end;

dom f = A by FUNCT_2:def 1;
then card (Union f) c= (card A) *` omega by A15, CARD_3:132;
hence card { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } in continuum by A14, A17, ORDINAL1:22, XBOOLE_1:1; :: thesis: verum