let U be Subset of REAL ; :: thesis: { x where x is Element of REAL : x is_local_minimum_of U } is countable
set X = { x where x is Element of REAL : x is_local_minimum_of U } ;
defpred S₁[ set , set ] means ex x, y being real number st
( $1 = x & $2 = ].y,x.[ & y < x & ].y,x.[ misses U );

A1: now

let a be set ; :: thesis: ( a in { x where x is Element of REAL : x is_local_minimum_of U } implies ex b being set st
( b in bool REAL & S₁[a,b] ) )
assume a in { x where x is Element of REAL : x is_local_minimum_of U } ; :: thesis: ex b being set st
( b in bool REAL & S₁[a,b] )
then consider x being Element of REAL such that
A2: ( a = x & x is_local_minimum_of U ) ;
ex y being real number st
( y < x & ].y,x.[ misses U ) by A2, Def3;
hence ex b being set st
( b in bool REAL & S₁[a,b] ) by A2; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = { x where x is Element of REAL : x is_local_minimum_of U } & rng f c= bool REAL ) and
A4: for a being set st a in { x where x is Element of REAL : x is_local_minimum_of U } holds
S₁[a,f . a] from WELLORD2:sch 1(A1);
A5: rng f is mutually-disjoint

proof

let a be set ; :: according to TAXONOM2:def 5 :: thesis: for b₁ being set holds
( not a in rng f or not b₁ in rng f or a = b₁ or a misses b₁ )
let b be set ; :: thesis: ( not a in rng f or not b in rng f or a = b or a misses b )
assume a in rng f ; :: thesis: ( not b in rng f or a = b or a misses b )
then consider a' being set such that
A6: ( a' in dom f & a = f . a' ) by FUNCT_1:def 5;
assume b in rng f ; :: thesis: ( a = b or a misses b )
then consider b' being set such that
A7: ( b' in dom f & b = f . b' ) by FUNCT_1:def 5;
consider xa, ya being real number such that
A8: ( a' = xa & a = ].ya,xa.[ & ya < xa & ].ya,xa.[ misses U ) by A3, A4, A6;
consider xb, yb being real number such that
A9: ( b' = xb & b = ].yb,xb.[ & yb < xb & ].yb,xb.[ misses U ) by A3, A4, A7;
assume A10: ( a <> b & a meets b ) ; :: thesis: contradiction
then consider c being set such that
A11: ( c in a & c in b ) by XBOOLE_0:3;
reconsider c = c as Element of REAL by A8, A11;
( ex x being Element of REAL st
( xa = x & x is_local_minimum_of U ) & ex x being Element of REAL st
( xb = x & x is_local_minimum_of U ) ) by A3, A6, A7, A8, A9;
then A12: ( xb in U & xa in U ) by Def3;
( yb < c & c < xa & ya < c & c < xb ) by A8, A9, A11, XXREAL_1:4;
then ( ( yb < xa & xa < xb ) or ( xa > xb & xb > ya ) ) by A6, A7, A8, A9, A10, XXREAL_0:1, XXREAL_0:2;
then ( xa in b or xb in a ) by A8, A9, XXREAL_1:4;
hence contradiction by A8, A9, A12, XBOOLE_0:3; :: thesis: verum

end;

now

let a be set ; :: thesis: ( a in rng f implies ex y, x being real number st
( y < x & ].y,x.[ c= a ) )
assume a in rng f ; :: thesis: ex y, x being real number st
( y < x & ].y,x.[ c= a )
then consider b being set such that
A13: ( b in dom f & a = f . b ) by FUNCT_1:def 5;
consider x, y being real number such that
A14: ( b = x & a = ].y,x.[ & y < x & ].y,x.[ misses U ) by A3, A4, A13;
take y = y; :: thesis: ex x being real number st
( y < x & ].y,x.[ c= a )
take x = x; :: thesis: ( y < x & ].y,x.[ c= a )
thus ( y < x & ].y,x.[ c= a ) by A14; :: thesis: verum

end;

then rng f is countable by A5, Th18;
then A15: card (rng f) c= omega by CARD_3:def 15;
f is one-to-one

proof

let a', b' be set ; :: according to FUNCT_1:def 8 :: thesis: ( not a' in dom f or not b' in dom f or not f . a' = f . b' or a' = b' )
set a = f . a';
set b = f . b';
assume that
A16: a' in dom f and
A17: b' in dom f ; :: thesis: ( not f . a' = f . b' or a' = b' )
consider xa, ya being real number such that
A18: ( a' = xa & f . a' = ].ya,xa.[ & ya < xa & ].ya,xa.[ misses U ) by A3, A4, A16;
consider xb, yb being real number such that
A19: ( b' = xb & f . b' = ].yb,xb.[ & yb < xb & ].yb,xb.[ misses U ) by A3, A4, A17;
assume A20: ( f . a' = f . b' & a' <> b' ) ; :: thesis: contradiction
consider c being rational number such that
A21: ( ya < c & c < xa ) by A18, RAT_1:22;
A22: c in f . a' by A18, A21, XXREAL_1:4;
( ex x being Element of REAL st
( xa = x & x is_local_minimum_of U ) & ex x being Element of REAL st
( xb = x & x is_local_minimum_of U ) ) by A3, A16, A17, A18, A19;
then A23: ( xb in U & xa in U ) by Def3;
( yb < c & c < xa & ya < c & c < xb ) by A18, A19, A20, A22, XXREAL_1:4;
then ( ( yb < xa & xa < xb ) or ( xa > xb & xb > ya ) ) by A18, A19, A20, XXREAL_0:1, XXREAL_0:2;
then ( xa in f . b' or xb in f . a' ) by A18, A19, XXREAL_1:4;
hence contradiction by A18, A19, A23, XBOOLE_0:3; :: thesis: verum

end;

then card { x where x is Element of REAL : x is_local_minimum_of U } c= card (rng f) by A3, CARD_1:26;
hence card { x where x is Element of REAL : x is_local_minimum_of U } c= omega by A15, XBOOLE_1:1; :: according to CARD_3:def 15 :: thesis: verum