deffunc H₁( set ) -> set = { x where x is Element of REAL : x is_local_minimum_of $1 } ;
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

A2: 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:20;
hence (card A) *` omega in continuum by ORDINAL3:8; :: thesis: verum

end;

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

then A4: card (card A) in omega by CARD_3:84;
0 in card A by A3, ORDINAL3:8;
hence (card A) *` omega in continuum by A4, Th30, CARD_4:16; :: thesis: verum

end;

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

then omega c= card A by CARD_5:16;
hence (card A) *` omega in continuum by A1, A5, CARD_4:16; :: thesis: verum

end;

end;

end;

set Y = { x where x is Element of REAL : ex U being set st
( U in A & x is_local_minimum_of U ) } ;
set X = { x where x is Element of REAL : ex U being set st
( U in UniCl A & x is_local_minimum_of U ) } ;
A6: 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
A7: for a being set st a in A holds
f . a = H₁(a) from FUNCT_2:sch 2(A6);
A8: { 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
A9: a = x and
A10: ex U being set st
( U in UniCl A & x is_local_minimum_of U ) ;
consider U being set such that
A11: U in UniCl A and
A12: x is_local_minimum_of U by A10;
reconsider U = U as Subset of REAL by A11;
consider B being Subset-Family of REAL such that
A13: B c= A and
A14: U = union B by A11, CANTOR_1:def 1;
x in U by A12, Def3;
then consider C being set such that
A15: x in C and
A16: C in B by A14, TARSKI:def 4;
consider y being real number such that
A17: y < x and
A18: ].y,x.[ misses U by A12, Def3;
reconsider C = C as Subset of REAL by A16;
].y,x.[ misses C

proof

assume not ].y,x.[ misses C ; :: thesis: contradiction
then consider b being set such that
A19: b in ].y,x.[ and
A20: b in C by XBOOLE_0:3;
b in U by A14, A16, A20, TARSKI:def 4;
hence contradiction by A18, A19, XBOOLE_0:3; :: thesis: verum

end;

then x is_local_minimum_of C by A17, A15, 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 A13, A16, A9; :: thesis: verum

end;

{ 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 )
A21: dom f = A by FUNCT_2:def 1;
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
A22: a = x and
A23: ex U being set st
( U in A & x is_local_minimum_of U ) ;
consider U being set such that
A24: U in A and
A25: x is_local_minimum_of U by A23;
A26: f . U = H₁(U) by A7, A24;
a in H₁(U) by A22, A25;
hence a in Union f by A26, A21, A24, CARD_5:2; :: 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 A8, XBOOLE_1:1;
then A27: 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:11;
A28: 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 A29: a in A ; :: thesis: card (f . a) c= omega
then reconsider b = a as Subset of REAL ;
f . a = H₁(b) by A7, A29;
then f . a is countable by Th19;
hence card (f . a) c= omega by CARD_3:def 14; :: thesis: verum

end;

dom f = A by FUNCT_2:def 1;
then card (Union f) c= (card A) *` omega by A28, CARD_2:86;
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 A27, A2, ORDINAL1:12, XBOOLE_1:1; :: thesis: verum