deffunc H_{1}( 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

( 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_{1}(a) in bool REAL

A7: for a being set st a in A holds

f . a = H_{1}(a)
from FUNCT_2:sch 11(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 ) }

( U in A & x is_local_minimum_of U ) } c= Union f

( U in UniCl A & x is_local_minimum_of U ) } c= Union f by A8;

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 object st a in A holds

card (f . a) c= omega

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

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 :: thesis: (card A) *` omega in continuum end;

set Y = { x where x is Element of REAL : ex U being set st per cases
( card A is empty or ( not card A is empty & card A is finite ) or card A is infinite )
;

end;

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

( 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

proof

consider f being Function of A,(bool REAL) such that
let a be set ; :: thesis: ( a in A implies H_{1}(a) in bool REAL )

H_{1}(a) c= REAL
_{1}(a) in bool REAL )
; :: thesis: verum

end;H

proof

hence
( a in A implies H
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in H_{1}(a) or b in REAL )

assume b in H_{1}(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;assume b in H

then ex x being Element of REAL st

( b = x & x is_local_minimum_of a ) ;

hence b in REAL ; :: thesis: verum

A7: for a being set st a in A holds

f . a = H

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

{ x where x is Element of REAL : ex U being set st
let a be object ; :: 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;

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 such that

A17: y < x and

A18: ].y,x.[ misses U by A12;

reconsider C = C as Subset of REAL by A16;

].y,x.[ misses C

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

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 such that

A17: y < x and

A18: ].y,x.[ misses U by A12;

reconsider C = C as Subset of REAL by A16;

].y,x.[ misses C

proof

then
x is_local_minimum_of C
by A17, A15;
assume
not ].y,x.[ misses C
; :: thesis: contradiction

then consider b being object 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 consider b being object 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

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

( U in A & x is_local_minimum_of U ) } c= Union f

proof

then
{ x where x is Element of REAL : ex U being set st
let a be object ; :: 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_{1}(U)
by A7, A24;

a in H_{1}(U)
by A22, A25;

hence a in Union f by A26, A21, A24, CARD_5:2; :: thesis: verum

end;( 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

a in H

hence a in Union f by A26, A21, A24, CARD_5:2; :: thesis: verum

( U in UniCl A & x is_local_minimum_of U ) } c= Union f by A8;

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 object st a in A holds

card (f . a) c= omega

proof

dom f = A
by FUNCT_2:def 1;
let a be object ; :: 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_{1}(b)
by A7, A29;

then f . a is countable by Th19;

hence card (f . a) c= omega ; :: thesis: verum

end;assume A29: a in A ; :: thesis: card (f . a) c= omega

then reconsider b = a as Subset of REAL ;

f . a = H

then f . a is countable by Th19;

hence card (f . a) c= omega ; :: thesis: verum

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