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

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

end;

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

let a9, b9 be object ; :: according to FUNCT_1:def 4 :: thesis:
set a = f . a9;
set b = f . b9;
assume that
A6: a9 in dom f and
A7: b9 in dom f ; :: thesis:
consider xb, yb being Real such that
A8: b9 = xb and
A9: f . b9 = ].yb,xb.[ and
yb < xb and
A10: ].yb,xb.[ misses U by A4, A5, A7;
ex x being Element of REAL st
( xb = x & x is_local_minimum_of U ) by A4, A7, A8;
then A11: xb in U ;
assume that
A12: f . a9 = f . b9 and
A13: a9 <> b9 ; :: thesis:
consider xa, ya being Real such that
A14: a9 = xa and
A15: f . a9 = ].ya,xa.[ and
A16: ya < xa and
A17: ].ya,xa.[ misses U by A4, A5, A6;
consider c being Rational such that
A18: ya < c and
A19: c < xa by A16, RAT_1:7;
A20: c in f . a9 by A15, A18, A19, XXREAL_1:4;
then A21: c < xb by A9, A12, XXREAL_1:4;
ex x being Element of REAL st
( xa = x & x is_local_minimum_of U ) by A4, A6, A14;
then A22: xa in U ;
yb < c by A9, A12, A20, XXREAL_1:4;
then ( ( yb < xa & xa < xb ) or ( xa > xb & xb > ya ) ) by A19, A18, A21, A14, A8, A13, XXREAL_0:1, XXREAL_0:2;
then ( xa in f . b9 or xb in f . a9 ) by A15, A9, XXREAL_1:4;
hence contradiction by A15, A17, A9, A10, A11, A22, XBOOLE_0:3; :: thesis:

end;

let a be set ; :: according to TAXONOM2:def 5 :: thesis:
let b be set ; :: thesis:
assume a in rng f ; :: thesis:
then consider a9 being object such that
A25: a9 in dom f and
A26: a = f . a9 by FUNCT_1:def 3;
consider xa, ya being Real such that
A27: a9 = xa and
A28: a = ].ya,xa.[ and
ya < xa and
A29: ].ya,xa.[ misses U by A4, A5, A25, A26;
ex x being Element of REAL st
( xa = x & x is_local_minimum_of U ) by A4, A25, A27;
then A30: xa in U ;
assume b in rng f ; :: thesis:
then consider b9 being object such that
A31: b9 in dom f and
A32: b = f . b9 by FUNCT_1:def 3;
consider xb, yb being Real such that
A33: b9 = xb and
A34: b = ].yb,xb.[ and
yb < xb and
A35: ].yb,xb.[ misses U by A4, A5, A31, A32;
assume that
A36: a <> b and
A37: a meets b ; :: thesis:
consider c being object such that
A38: c in a and
A39: c in b by A37, XBOOLE_0:3;
reconsider c = c as Element of REAL by A28, A38;
A40: c < xa by A28, A38, XXREAL_1:4;
ex x being Element of REAL st
( xb = x & x is_local_minimum_of U ) by A4, A31, A33;
then A41: xb in U ;
A42: c < xb by A34, A39, XXREAL_1:4;
A43: ya < c by A28, A38, XXREAL_1:4;
yb < c by A34, A39, XXREAL_1:4;
then ( ( yb < xa & xa < xb ) or ( xa > xb & xb > ya ) ) by A40, A43, A42, A26, A32, A27, A33, A36, XXREAL_0:1, XXREAL_0:2;
then ( xa in b or xb in a ) by A28, A34, XXREAL_1:4;
hence contradiction by A28, A29, A34, A35, A41, A30, XBOOLE_0:3; :: thesis:

end;

let a be set ; :: thesis:
assume a in rng f ; :: thesis:
then consider b being object such that
A44: b in dom f and
A45: a = f . b by FUNCT_1:def 3;
consider x, y being Real such that
b = x and
A46: a = ].y,x.[ and
A47: y < x and
].y,x.[ misses U by A4, A5, A44, A45;
take y = y; :: thesis:
take x = x; :: thesis:
thus ( y < x & ].y,x.[ c= a ) by A46, A47; :: thesis:

end;