:: RCOMP_1 semantic presentation

REAL is non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() set

K19(REAL) is set
COMPLEX is non empty V50() V56() V57() set
RAT is non empty V50() V51() V52() V53() V56() V57() set
INT is non empty V50() V51() V52() V53() V54() V56() V57() set

K19(omega) is set
K19(NAT) is set

K19(K20(COMPLEX,COMPLEX)) is set

K19(K20(COMPLEX,REAL)) is set

K19(K20(REAL,REAL)) is set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K19(K20(K20(REAL,REAL),REAL)) is set

K19(K20(RAT,RAT)) is set

K19(K20(K20(RAT,RAT),RAT)) is set

K19(K20(INT,INT)) is set

K19(K20(K20(INT,INT),INT)) is set

K19(K20(K20(NAT,NAT),NAT)) is set
{} is set

K19(K20(NAT,REAL)) is set

K19(K20(NAT,NAT)) is set

ExtREAL is non empty V51() V71() set
g is V30() real ext-real set
s is V30() real ext-real set
[.g,s.] is V71() set
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & b1 <= s ) } is set
Y is set

{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & b1 <= s ) } is set
X is V50() V51() V52() Element of K19(REAL)
e is set

e is set
r is V30() real ext-real Element of REAL
g is ext-real set
s is ext-real set
].g,s.[ is non left_end non right_end V71() set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g & not s <= b1 ) } is set
Y is set

{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g & not s <= b1 ) } is set
X is V50() V51() V52() Element of K19(REAL)
e is set
r is V30() real ext-real Element of REAL
e is set

g is V30() real ext-real set
s is V30() real ext-real set
g - s is V30() real ext-real set
abs (g - s) is V30() real ext-real Element of REAL
Y is V30() real ext-real set
s - Y is V30() real ext-real set
s + Y is V30() real ext-real set
((s - Y),(s + Y)) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s - Y & not s + Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s - Y & not s + Y <= b1 ) } is set
- Y is V30() real ext-real set
s + (- Y) is V30() real ext-real set
X is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
- Y is V30() real ext-real set
s + (- Y) is V30() real ext-real set
g is V30() real ext-real set
2 * g is V30() real ext-real Element of REAL
s is V30() real ext-real set
Y is V30() real ext-real set
(s,Y) is V50() V51() V52() V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= Y ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( s <= b1 & b1 <= Y ) } is set
s + Y is V30() real ext-real set
(s + Y) - (2 * g) is V30() real ext-real Element of REAL
abs ((s + Y) - (2 * g)) is V30() real ext-real Element of REAL
Y - s is V30() real ext-real set
2 * Y is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
- (2 * Y) is V30() real ext-real Element of REAL
- (2 * g) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * Y)) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * g)) is V30() real ext-real Element of REAL
- (Y - s) is V30() real ext-real set
2 * s is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
- (2 * s) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * s)) is V30() real ext-real Element of REAL
- (Y - s) is V30() real ext-real set
s - Y is V30() real ext-real set
(s - Y) + (2 * g) is V30() real ext-real Element of REAL
(s + Y) - (s - Y) is V30() real ext-real set
1 / 2 is V30() real ext-real non negative Element of REAL
(1 / 2) * (2 * g) is V30() real ext-real Element of REAL
2 * Y is V30() real ext-real Element of REAL
(1 / 2) * (2 * Y) is V30() real ext-real Element of REAL
(2 * g) + (Y - s) is V30() real ext-real Element of REAL
(s + Y) - (Y - s) is V30() real ext-real set
2 * s is V30() real ext-real Element of REAL
(1 / 2) * (2 * s) is V30() real ext-real Element of REAL
g is V30() real ext-real set
2 * g is V30() real ext-real Element of REAL
s is V30() real ext-real set
Y is V30() real ext-real set
(s,Y) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s & not Y <= b1 ) } is set
Y - s is V30() real ext-real set
s + Y is V30() real ext-real set
(s + Y) - (2 * g) is V30() real ext-real Element of REAL
abs ((s + Y) - (2 * g)) is V30() real ext-real Element of REAL
2 * Y is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
- (2 * g) is V30() real ext-real Element of REAL
- (2 * Y) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * g)) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * Y)) is V30() real ext-real Element of REAL
- (Y - s) is V30() real ext-real set
2 * s is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
- (2 * s) is V30() real ext-real Element of REAL
(s + Y) + (- (2 * s)) is V30() real ext-real Element of REAL
- (Y - s) is V30() real ext-real set
s - Y is V30() real ext-real set
(s - Y) + (2 * g) is V30() real ext-real Element of REAL
(s + Y) - (s - Y) is V30() real ext-real set
1 / 2 is V30() real ext-real non negative Element of REAL
2 * Y is V30() real ext-real Element of REAL
(1 / 2) * (2 * Y) is V30() real ext-real Element of REAL
(1 / 2) * (2 * g) is V30() real ext-real Element of REAL
(2 * g) + (Y - s) is V30() real ext-real Element of REAL
(s + Y) - (Y - s) is V30() real ext-real set
2 * s is V30() real ext-real Element of REAL
(1 / 2) * (2 * s) is V30() real ext-real Element of REAL
g is V30() real ext-real set
s is V30() real ext-real set
(g,s) is V50() V51() V52() V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & b1 <= s ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & b1 <= s ) } is set

rng Y is V50() V51() V52() set
s + 1 is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
e is V30() real ext-real set
r is V30() real ext-real Element of REAL

Y . e is V30() real ext-real Element of REAL
dom Y is set

Y . e is V30() real ext-real Element of REAL
g - 1 is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
X + 1 is V30() real ext-real Element of REAL
1 - 1 is V30() real ext-real Element of REAL
g - (1 - 1) is V30() real ext-real Element of REAL
e is V30() real ext-real set
r is V30() real ext-real Element of REAL

Y . e is V30() real ext-real Element of REAL
dom Y is set

Y . e is V30() real ext-real Element of REAL
g is V30() real ext-real set
s is V30() real ext-real set
(g,s) is V50() V51() V52() V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & b1 <= s ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & b1 <= s ) } is set

rng Y is V50() V51() V52() set

{g} is V50() V51() V52() set

K19(K20(NAT,{g})) is set

dom Y is set
Y . e is V30() real ext-real Element of REAL

X . e is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
X . 0 is V30() real ext-real Element of REAL

{s} is V50() V51() V52() set

K19(K20(NAT,{s})) is set

dom Y is set
Y . e is V30() real ext-real Element of REAL

X . e is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
X . 0 is V30() real ext-real Element of REAL

g is V30() real ext-real set
s is V30() real ext-real set
(g,s) is V50() V51() V52() V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & b1 <= s ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & b1 <= s ) } is set

rng Y is V50() V51() V52() set

rng X is V50() V51() V52() set

g is V30() real ext-real set
s is V30() real ext-real set
(g,s) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g & not s <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g & not s <= b1 ) } is set
Y is V50() V51() V52() Element of K19(REAL)

rng X is V50() V51() V52() set

(lim X) - g is V30() real ext-real Element of REAL

s - (lim X) is V30() real ext-real Element of REAL

X . g1 is V30() real ext-real Element of REAL
(X . g1) - (lim X) is V30() real ext-real Element of REAL
abs ((X . g1) - (lim X)) is V30() real ext-real Element of REAL
- (abs ((X . g1) - (lim X))) is V30() real ext-real Element of REAL
- ((X . g1) - (lim X)) is V30() real ext-real Element of REAL
- (- (abs ((X . g1) - (lim X)))) is V30() real ext-real Element of REAL
- (- ((X . g1) - (lim X))) is V30() real ext-real Element of REAL
- ((lim X) - g) is V30() real ext-real Element of REAL
g - (lim X) is V30() real ext-real Element of REAL
dom X is set
X is V30() real ext-real set
(g,s) ` is V50() V51() V52() Element of K19(REAL)
REAL \ (g,s) is V50() V51() V52() set
X is V30() real ext-real set
e is V30() real ext-real Element of REAL
g is V30() real ext-real set
s is V30() real ext-real set
(g,s) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g & not s <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g & not s <= b1 ) } is set
Y is V50() V51() V52() Element of K19(REAL)
(g,s) is V50() V51() V52() V71() Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & b1 <= s ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & b1 <= s ) } is set
Y is V50() V51() V52() Element of K19(REAL)
g is V50() V51() V52() Element of K19(REAL)

rng s is V50() V51() V52() set

g is V50() V51() V52() Element of K19(REAL)

s is V50() V51() V52() Element of K19(REAL)

X is V30() real ext-real set

(e + 1) + r is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT
(g * g1) . ((e + 1) + r) is V30() real ext-real Element of REAL
((g * g1) . ((e + 1) + r)) - (lim Y) is V30() real ext-real Element of REAL
abs (((g * g1) . ((e + 1) + r)) - (lim Y)) is V30() real ext-real Element of REAL
g1 . ((e + 1) + r) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT
g . (g1 . ((e + 1) + r)) is V30() real ext-real Element of REAL
(g . (g1 . ((e + 1) + r))) - (lim Y) is V30() real ext-real Element of REAL
abs ((g . (g1 . ((e + 1) + r))) - (lim Y)) is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)

Y is ext-real set

s . Y is V30() real ext-real Element of REAL
X is V30() real ext-real set
Y is V30() real ext-real set
X is V30() real ext-real set
e is V30() real ext-real set
Y + 1 is V30() real ext-real Element of REAL

s . g2 is V30() real ext-real Element of REAL
(s . g2) - Y is V30() real ext-real Element of REAL
abs ((s . g2) - Y) is V30() real ext-real Element of REAL
rng s is V50() V51() V52() set
Y is set
dom s is set
X is set
s . X is V30() real ext-real Element of REAL

s . e is V30() real ext-real Element of REAL

- s is V30() real ext-real non positive Element of REAL
Y is ext-real set

s . Y is V30() real ext-real Element of REAL
- Y is V30() real ext-real non positive Element of REAL
X is V30() real ext-real set
Y is V30() real ext-real set
X is V30() real ext-real set
e is V30() real ext-real set
Y - 1 is V30() real ext-real Element of REAL
abs (Y - 1) is V30() real ext-real Element of REAL

s . g2 is V30() real ext-real Element of REAL
(s . g2) - Y is V30() real ext-real Element of REAL
abs ((s . g2) - Y) is V30() real ext-real Element of REAL
- g1 is V30() real ext-real non positive Element of REAL
- g2 is V30() real ext-real non positive Element of REAL
- r is V30() real ext-real non positive Element of REAL
(s . g2) + 1 is V30() real ext-real Element of REAL
Y - (s . g2) is V30() real ext-real Element of REAL
- ((s . g2) - Y) is V30() real ext-real Element of REAL
abs (- ((s . g2) - Y)) is V30() real ext-real Element of REAL
rng s is V50() V51() V52() set
Y is set
dom s is set
X is set
s . X is V30() real ext-real Element of REAL

s . e is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

rng s is V50() V51() V52() set
Y is V30() real ext-real set
X is V30() real ext-real set
Y - 1 is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
X + 1 is V30() real ext-real Element of REAL
1 - 1 is V30() real ext-real Element of REAL
Y - (1 - 1) is V30() real ext-real Element of REAL
e is V30() real ext-real set

s . e is V30() real ext-real Element of REAL
dom s is set

s . e is V30() real ext-real Element of REAL
Y is V30() real ext-real set
X is V30() real ext-real set
Y + 1 is V30() real ext-real Element of REAL
X is V30() real ext-real Element of REAL
e is V30() real ext-real set

s . e is V30() real ext-real Element of REAL
dom s is set

s . e is V30() real ext-real Element of REAL

rng Y is V50() V51() V52() set

g is V50() V51() V52() Element of K19(REAL)

1 / (Y + 1) is V30() real ext-real non negative Element of REAL
(Y + 1) " is non empty V30() real ext-real positive non negative Element of REAL
() - (1 / (Y + 1)) is V30() real ext-real Element of REAL
X is V30() real ext-real set
X + (1 / (Y + 1)) is V30() real ext-real Element of REAL
() - X is V30() real ext-real Element of REAL

Y . X is V30() real ext-real Element of REAL

1 / (X + 1) is V30() real ext-real non negative Element of REAL
() - (Y . X) is V30() real ext-real Element of REAL
e is V30() real ext-real set
() - e is V30() real ext-real Element of REAL
rng Y is V50() V51() V52() set
X is set
dom Y is set
e is set
Y . e is V30() real ext-real Element of REAL

Y . r is V30() real ext-real Element of REAL
X is V30() real ext-real set
X " is V30() real ext-real set

1 / (g1 + 1) is V30() real ext-real non negative Element of REAL
1 / (r + 1) is V30() real ext-real non negative Element of REAL
Y . g1 is V30() real ext-real Element of REAL
() - (Y . g1) is V30() real ext-real Element of REAL

(X ") + 0 is V30() real ext-real Element of REAL
1 / (X ") is V30() real ext-real Element of REAL
1 / (e + 1) is V30() real ext-real non negative Element of REAL
(Y . g1) - () is V30() real ext-real Element of REAL
- ((Y . g1) - ()) is V30() real ext-real Element of REAL
abs (- ((Y . g1) - ())) is V30() real ext-real Element of REAL
abs ((Y . g1) - ()) is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

1 / (Y + 1) is V30() real ext-real non negative Element of REAL
(Y + 1) " is non empty V30() real ext-real positive non negative Element of REAL
() + (1 / (Y + 1)) is V30() real ext-real Element of REAL
X is V30() real ext-real set
X - () is V30() real ext-real Element of REAL

Y . X is V30() real ext-real Element of REAL

1 / (X + 1) is V30() real ext-real non negative Element of REAL
(Y . X) - () is V30() real ext-real Element of REAL
e is V30() real ext-real set
e - () is V30() real ext-real Element of REAL
rng Y is V50() V51() V52() set
X is set
dom Y is set
e is set
Y . e is V30() real ext-real Element of REAL

Y . r is V30() real ext-real Element of REAL
X is V30() real ext-real set
X " is V30() real ext-real set

1 / (g1 + 1) is V30() real ext-real non negative Element of REAL
1 / (r + 1) is V30() real ext-real non negative Element of REAL
Y . g1 is V30() real ext-real Element of REAL
(Y . g1) - () is V30() real ext-real Element of REAL

(X ") + 0 is V30() real ext-real Element of REAL
1 / (X ") is V30() real ext-real Element of REAL
1 / (e + 1) is V30() real ext-real non negative Element of REAL
abs ((Y . g1) - ()) is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

g is V50() V51() V52() Element of K19(REAL)
(1,0) is V50() V51() V52() V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( 1 <= b1 & b1 <= 0 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( 1 <= b1 & b1 <= 0 ) } is set

s is V30() real ext-real Element of REAL

Y is V30() real ext-real Element of REAL
(s,Y) is V50() V51() V52() V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( s <= b1 & b1 <= Y ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( s <= b1 & b1 <= Y ) } is set
X is V30() real ext-real Element of REAL
(0,1) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= 0 & not 1 <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= 0 & not 1 <= b1 ) } is set
g is V30() real ext-real set
g - 1 is V30() real ext-real Element of REAL
g + 1 is V30() real ext-real Element of REAL
((g - 1),(g + 1)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - 1 & not g + 1 <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - 1 & not g + 1 <= b1 ) } is set
g is V30() real ext-real set
s is V50() V51() V52() (g)
Y is V30() real ext-real set
g - Y is V30() real ext-real set
g + Y is V30() real ext-real set
((g - Y),(g + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - Y & not g + Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - Y & not g + Y <= b1 ) } is set
g is V30() real ext-real set
s is V50() V51() V52() () (g)
g - g is V30() real ext-real set
abs (g - g) is V30() real ext-real Element of REAL
Y is V30() real ext-real set
g - Y is V30() real ext-real set
g + Y is V30() real ext-real set
((g - Y),(g + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - Y & not g + Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - Y & not g + Y <= b1 ) } is set
g is V30() real ext-real set
s is V50() V51() V52() () (g)
Y is V50() V51() V52() () (g)
X is V30() real ext-real set
g - X is V30() real ext-real set
g + X is V30() real ext-real set
((g - X),(g + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - X & not g + X <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - X & not g + X <= b1 ) } is set
e is V30() real ext-real set
g - e is V30() real ext-real set
g + e is V30() real ext-real set
((g - e),(g + e)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - e & not g + e <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - e & not g + e <= b1 ) } is set
min (X,e) is V30() real ext-real set
g - (min (X,e)) is V30() real ext-real set
g + (min (X,e)) is V30() real ext-real set
((g - (min (X,e))),(g + (min (X,e)))) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g - (min (X,e)) & not g + (min (X,e)) <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g - (min (X,e)) & not g + (min (X,e)) <= b1 ) } is set
g1 is V50() V51() V52() () (g)
- X is V30() real ext-real set
- (min (X,e)) is V30() real ext-real set
g + (- X) is V30() real ext-real set
g + (- (min (X,e))) is V30() real ext-real set
- e is V30() real ext-real set
g + (- e) is V30() real ext-real set
g2 is set
m is V30() real ext-real Element of REAL
c10 is V30() real ext-real Element of REAL
g2 is set
m is V30() real ext-real Element of REAL
c10 is V30() real ext-real Element of REAL
g is V50() V51() V52() () Element of K19(REAL)
s is V30() real ext-real set
g ` is V50() V51() V52() Element of K19(REAL)
REAL \ g is V50() V51() V52() set
Y is V50() V51() V52() () (s)
X is V30() real ext-real set
s - X is V30() real ext-real set
s + X is V30() real ext-real set
((s - X),(s + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s - X & not s + X <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s - X & not s + X <= b1 ) } is set
e is set
r is V30() real ext-real Element of REAL
g1 is V30() real ext-real Element of REAL

1 / (Y + 1) is V30() real ext-real non negative Element of REAL
s - (1 / (Y + 1)) is V30() real ext-real Element of REAL
s + (1 / (Y + 1)) is V30() real ext-real Element of REAL
((s - (1 / (Y + 1))),(s + (1 / (Y + 1)))) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s - (1 / (Y + 1)) & not s + (1 / (Y + 1)) <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s - (1 / (Y + 1)) & not s + (1 / (Y + 1)) <= b1 ) } is set
(Y + 1) " is non empty V30() real ext-real positive non negative Element of REAL
1 * ((Y + 1) ") is V30() real ext-real non negative Element of REAL
X is V50() V51() V52() () (s)
e is V30() real ext-real Element of REAL

X . r is V30() real ext-real Element of REAL
Y . r is V30() real ext-real Element of REAL
e . r is V30() real ext-real Element of REAL

1 / (r + 1) is V30() real ext-real non negative Element of REAL
s - (1 / (r + 1)) is V30() real ext-real Element of REAL
s + (1 / (r + 1)) is V30() real ext-real Element of REAL
((s - (1 / (r + 1))),(s + (1 / (r + 1)))) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s - (1 / (r + 1)) & not s + (1 / (r + 1)) <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s - (1 / (r + 1)) & not s + (1 / (r + 1)) <= b1 ) } is set
g1 is V30() real ext-real Element of REAL
g1 is V30() real ext-real Element of REAL
rng Y is V50() V51() V52() set
r is set
dom Y is set
g1 is set
Y . g1 is V30() real ext-real Element of REAL

Y . g2 is V30() real ext-real Element of REAL
r is V30() real ext-real set
r " is V30() real ext-real set

1 / (m + 1) is V30() real ext-real non negative Element of REAL
1 / (g2 + 1) is V30() real ext-real non negative Element of REAL
(r ") + 0 is V30() real ext-real Element of REAL
1 / (r ") is V30() real ext-real Element of REAL
e . m is V30() real ext-real Element of REAL
(e . m) - s is V30() real ext-real Element of REAL
abs ((e . m) - s) is V30() real ext-real Element of REAL
s + (1 / (m + 1)) is V30() real ext-real Element of REAL
(s + (1 / (m + 1))) - s is V30() real ext-real Element of REAL
abs ((s + (1 / (m + 1))) - s) is V30() real ext-real Element of REAL

r is V30() real ext-real set
r " is V30() real ext-real set

1 / (m + 1) is V30() real ext-real non negative Element of REAL
1 / (g2 + 1) is V30() real ext-real non negative Element of REAL
(r ") + 0 is V30() real ext-real Element of REAL
1 / (r ") is V30() real ext-real Element of REAL
X . m is V30() real ext-real Element of REAL
(X . m) - s is V30() real ext-real Element of REAL
abs ((X . m) - s) is V30() real ext-real Element of REAL
s - (1 / (m + 1)) is V30() real ext-real Element of REAL
(s - (1 / (m + 1))) - s is V30() real ext-real Element of REAL
abs ((s - (1 / (m + 1))) - s) is V30() real ext-real Element of REAL
- (1 / (m + 1)) is V30() real ext-real non positive Element of REAL
abs (- (1 / (m + 1))) is V30() real ext-real Element of REAL
abs (1 / (m + 1)) is V30() real ext-real Element of REAL

g is V50() V51() V52() () Element of K19(REAL)
s is V30() real ext-real set
Y is V50() V51() V52() () (s)
X is V30() real ext-real set
s - X is V30() real ext-real set
s + X is V30() real ext-real set
((s - X),(s + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s - X & not s + X <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s - X & not s + X <= b1 ) } is set
g is V50() V51() V52() Element of K19(REAL)
g ` is V50() V51() V52() Element of K19(REAL)
REAL \ g is V50() V51() V52() set

rng s is V50() V51() V52() set

Y is V50() V51() V52() () ( lim s)
X is V30() real ext-real set
(lim s) - X is V30() real ext-real Element of REAL
(lim s) + X is V30() real ext-real Element of REAL
(((lim s) - X),((lim s) + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= (lim s) - X & not (lim s) + X <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= (lim s) - X & not (lim s) + X <= b1 ) } is set

dom s is set
s . e is V30() real ext-real Element of REAL
(s . e) - (lim s) is V30() real ext-real Element of REAL
abs ((s . e) - (lim s)) is V30() real ext-real Element of REAL
- X is V30() real ext-real set
(lim s) + ((s . e) - (lim s)) is V30() real ext-real Element of REAL
(lim s) + (- X) is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)

s is V50() V51() V52() () ( upper_bound g)
Y is V30() real ext-real set
() - Y is V30() real ext-real Element of REAL
() + Y is V30() real ext-real Element of REAL
((() - Y),(() + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= () - Y & not () + Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= () - Y & not () + Y <= b1 ) } is set
Y / 2 is V30() real ext-real Element of REAL
() + (Y / 2) is V30() real ext-real Element of REAL
(() + (Y / 2)) + (Y / 2) is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)

s is V50() V51() V52() () ( lower_bound g)
Y is V30() real ext-real set
() - Y is V30() real ext-real Element of REAL
() + Y is V30() real ext-real Element of REAL
((() - Y),(() + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= () - Y & not () + Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= () - Y & not () + Y <= b1 ) } is set
Y / 2 is V30() real ext-real Element of REAL
() - (Y / 2) is V30() real ext-real Element of REAL
(() - (Y / 2)) - (Y / 2) is V30() real ext-real Element of REAL
g is V50() V51() V52() Element of K19(REAL)
(1,0) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= 1 & not 0 <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= 1 & not 0 <= b1 ) } is set

s is V30() real ext-real Element of REAL

Y is V30() real ext-real Element of REAL
(s,Y) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= s & not Y <= b1 ) } is set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= s & not Y <= b1 ) } is set
X is V30() real ext-real Element of REAL
Y - X is V30() real ext-real Element of REAL
e is V30() real ext-real Element of REAL
Y - (Y - X) is V30() real ext-real Element of REAL
e is V30() real ext-real set
X - s is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s + (X - s) is V30() real ext-real Element of REAL
r is V30() real ext-real set
g1 is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : ( g1 <= b1 & b1 <= g2 ) } is set
(g1,g2) is V50() V51() V52() V71() () Element of K19(REAL)
{ b1 where b1 is ext-real Element of ExtREAL : ( g1 <= b1 & b1 <= g2 ) } is set
g is V30() real ext-real set
s is ext-real set
[.g,s.[ is non right_end V71() set
{ b1 where b1 is ext-real Element of ExtREAL : ( g <= b1 & not s <= b1 ) } is set
Y is set

{ b1 where b1 is V30() real ext-real Element of REAL : ( g <= b1 & not s <= b1 ) } is set
X is V50() V51() V52() Element of K19(REAL)
e is set

e is set
r is V30() real ext-real Element of REAL
g is ext-real set
s is V30() real ext-real set
].g,s.] is non left_end V71() set
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= g & b1 <= s ) } is set
Y is set

{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= g & b1 <= s ) } is set
X is V50() V51() V52() Element of K19(REAL)
e is set

e is set
r is V30() real ext-real Element of REAL