:: RAT_1 semantic presentation

REAL is non empty set

RAT+ is non empty set

{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } is set

{ [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : verum } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : verum } is Element of bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) }
bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } is set
( { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : verum } ) \/ omega is non empty set

bool () is set
DEDEKIND_CUTS is non empty Element of bool ()
REAL+ is non empty set
COMPLEX is non empty set
INT is non empty set

is non empty set

REAL+ \/ is non empty set
is set
is non empty set
is non empty set
is non empty set
() \ is Element of bool ()
bool () is set
RAT is non empty set

RAT+ \/ is non empty set
() \ is Element of bool ()
bool () is set

is non empty set

{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : verum } is Element of bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) }
bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } is set
( { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer Element of omega : verum } ) \/ omega is non empty set

09 / p is Element of RAT+
09 / p is ext-real non negative V31() real Element of REAL
p " is ext-real non negative V31() real set
09 * (p ") is ext-real non negative V31() real set

+ (0,()) is ext-real V31() real Element of REAL
p " is ext-real non negative V31() real Element of REAL
p * (p ") is ext-real non negative V31() real Element of REAL
s is ext-real V31() real Element of REAL
r is ext-real V31() real Element of REAL
[*s,r*] is Element of COMPLEX
k is ext-real V31() real Element of REAL
m is ext-real V31() real Element of REAL
[*k,m*] is Element of COMPLEX
* (s,k) is ext-real V31() real Element of REAL
* (r,m) is ext-real V31() real Element of REAL
opp (* (r,m)) is ext-real V31() real Element of REAL
+ ((* (s,k)),(opp (* (r,m)))) is ext-real V31() real Element of REAL
* (s,m) is ext-real V31() real Element of REAL
* (r,k) is ext-real V31() real Element of REAL
+ ((* (s,m)),(* (r,k))) is ext-real V31() real Element of REAL
[*(+ ((* (s,k)),(opp (* (r,m))))),(+ ((* (s,m)),(* (r,k))))*] is Element of COMPLEX
+ ((* (s,k)),()) is ext-real V31() real Element of REAL
l is Element of RAT+
z is Element of RAT+
l *' z is Element of RAT+

(() *^ ()) / (() *^ ()) is Element of RAT+
x9 is Element of REAL+
y9 is Element of REAL+
x9 *' y9 is Element of REAL+
xx1 is ext-real V31() real Element of REAL
yy1 is ext-real V31() real Element of REAL
* (xx1,yy1) is ext-real V31() real Element of REAL
a is Element of REAL+
b is Element of REAL+
a *' b is Element of REAL+
x91 is Element of RAT+
x92 is Element of RAT+
x91 *' x92 is Element of RAT+

((numerator x91) *^ (numerator x92)) / ((denominator x91) *^ (denominator x92)) is Element of RAT+
09 * (p ") is ext-real non negative V31() real Element of REAL
x91 is ext-real V31() real Element of REAL
x92 is ext-real V31() real Element of REAL
[*x91,x92*] is Element of COMPLEX
y91 is ext-real V31() real Element of REAL
y92 is ext-real V31() real Element of REAL
[*y91,y92*] is Element of COMPLEX
* (x91,y91) is ext-real V31() real Element of REAL
* (x92,y92) is ext-real V31() real Element of REAL
opp (* (x92,y92)) is ext-real V31() real Element of REAL
+ ((* (x91,y91)),(opp (* (x92,y92)))) is ext-real V31() real Element of REAL
* (x91,y92) is ext-real V31() real Element of REAL
* (x92,y91) is ext-real V31() real Element of REAL
+ ((* (x91,y92)),(* (x92,y91))) is ext-real V31() real Element of REAL
[*(+ ((* (x91,y91)),(opp (* (x92,y92))))),(+ ((* (x91,y92)),(* (x92,y91))))*] is Element of COMPLEX
x19 is Element of REAL+
y19 is Element of REAL+
x19 *' y19 is Element of REAL+
* (x91,k) is ext-real V31() real Element of REAL
* (x92,0) is ext-real V31() real Element of REAL
opp (* (x92,0)) is ext-real V31() real Element of REAL
+ ((* (x91,k)),(opp (* (x92,0)))) is ext-real V31() real Element of REAL
+ ((* (x91,k)),0) is ext-real V31() real Element of REAL
x9 is Element of REAL+
y9 is Element of REAL+
x9 *' y9 is Element of REAL+
x99 is Element of RAT+
y99 is Element of RAT+
x99 *' y99 is Element of RAT+

((numerator x99) *^ (numerator y99)) / ((denominator x99) *^ (denominator y99)) is Element of RAT+
a is Element of RAT+
b is Element of RAT+
a *' b is Element of RAT+

(() *^ ()) / (() *^ ()) is Element of RAT+
p / one is Element of RAT+
(09 / p) *' (p / one) is Element of RAT+

((numerator (09 / p)) *^ (numerator (p / one))) / ((denominator (09 / p)) *^ (denominator (p / one))) is Element of RAT+

(09 *^ p) / () is Element of RAT+
09 / one is Element of RAT+
p / p is Element of RAT+
(09 / one) *' (p / p) is Element of RAT+

((numerator (09 / one)) *^ (numerator (p / p))) / ((denominator (09 / one)) *^ (denominator (p / p))) is Element of RAT+
(09 / one) *' one is Element of RAT+

((numerator (09 / one)) *^ ()) / ((denominator (09 / one)) *^ ) is Element of RAT+
x99 *' one is Element of RAT+

((numerator x99) *^ ()) / ((denominator x99) *^ ) is Element of RAT+
(x99 *' y99) *' b is Element of RAT+

((numerator (x99 *' y99)) *^ ()) / ((denominator (x99 *' y99)) *^ ()) is Element of RAT+
c26 is Element of RAT+
c27 is Element of RAT+
c26 *' c27 is Element of RAT+

((numerator c26) *^ (numerator c27)) / ((denominator c26) *^ (denominator c27)) is Element of RAT+
09 is Element of REAL+
p is ext-real V31() real set
- p is ext-real V31() real set
q is Element of REAL+
09 - q is set
q -' 09 is Element of REAL+
[{},(q -' 09)] is set
{{},(q -' 09)} is non empty set
is non empty set
{{{},(q -' 09)},} is non empty set
[0,0] is set
{0,0} is non empty set
is non empty set
is non empty set
(q -' 09) + 09 is Element of REAL+
REAL+ \/ is non empty set
r is ext-real V31() real Element of REAL
p + r is ext-real V31() real Element of REAL
k is ext-real V31() real Element of REAL
m is ext-real V31() real Element of REAL
[*k,m*] is Element of COMPLEX
l is ext-real V31() real Element of REAL
z is ext-real V31() real Element of REAL
[*l,z*] is Element of COMPLEX
+ (k,l) is ext-real V31() real Element of REAL
+ (m,z) is ext-real V31() real Element of REAL
[*(+ (k,l)),(+ (m,z))*] is Element of COMPLEX
x9 is Element of REAL+
y9 is Element of REAL+
[0,y9] is set
{0,y9} is non empty set
{{0,y9},} is non empty set
x9 - y9 is set
p is set
q is Element of RAT+

() / () is ext-real non negative V31() real set
() " is ext-real non negative V31() real set
() * (() ") is ext-real non negative V31() real set
() / () is Element of RAT+

[0,0] is set
{0,0} is non empty set
is non empty set
is non empty set
q is set
s is set
[q,s] is set
{q,s} is non empty set
{q} is non empty set
{{q,s},{q}} is non empty set
r is Element of RAT+
k is Element of REAL+
[0,k] is set
{0,k} is non empty set
{{0,k},} is non empty set

- () is ext-real non positive V31() real integer set

m / l is ext-real non positive V31() real set
l " is ext-real non negative V31() real set
m * (l ") is ext-real non positive V31() real set
() / () is Element of RAT+
() / l is ext-real non negative V31() real set
() * (l ") is ext-real non negative V31() real set
09 - k is set
- (() / l) is ext-real non positive V31() real set

p is set

s / q is ext-real V31() real Element of REAL
q " is ext-real non negative V31() real set
s * (q ") is ext-real V31() real set
[0,0] is set
{0,0} is non empty set
is non empty set
is non empty set

s * () is ext-real V31() real integer Element of REAL

RAT+ \/ is non empty set

r / q is Element of RAT+

RAT+ \/ is non empty set

r / q is ext-real non negative V31() real Element of REAL
r * (q ") is ext-real non negative V31() real set
r / q is Element of RAT+
- (r / q) is ext-real non positive V31() real Element of REAL
k is Element of REAL+
09 - k is set
[0,k] is set
{0,k} is non empty set
{{0,k},} is non empty set

RAT+ \/ is non empty set

p is set

q / s is ext-real V31() real set
s " is ext-real V31() real set
q * (s ") is ext-real V31() real set

(- q) / r is ext-real V31() real Element of REAL
r " is ext-real non negative V31() real set
(- q) * (r ") is ext-real V31() real set
p is set
q is set
s is set

r / k is ext-real V31() real set
k " is ext-real V31() real set
r * (k ") is ext-real V31() real set
q is set

s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set
q is set

s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set

p / q is ext-real V31() real set
q " is ext-real V31() real set
p * (q ") is ext-real V31() real set
s is ext-real V31() real set

p / q is ext-real V31() real set
q " is ext-real V31() real set
p * (q ") is ext-real V31() real set
s is ext-real V31() real set
p is set

1 " is non empty ext-real positive non negative V31() real set

q / s is ext-real V31() real set
s " is ext-real V31() real set
q * (s ") is ext-real V31() real set
p is set
p is set

p / q is ext-real V31() real set
q " is ext-real V31() real set
p * (q ") is ext-real V31() real set
p is set

q / 1 is ext-real V31() real Element of REAL
1 " is non empty ext-real positive non negative V31() real set
q * (1 ") is ext-real V31() real set
p is ext-real V31() real () set
q is ext-real V31() real () set
p * q is ext-real V31() real set
r is ext-real V31() real integer () set
s is ext-real V31() real integer () set
s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set
m is ext-real V31() real integer () set
k is ext-real V31() real integer () set
k / m is ext-real V31() real set
m " is ext-real V31() real set
k * (m ") is ext-real V31() real set
k * s is ext-real V31() real integer () set
m * r is ext-real V31() real integer () set
(k * s) / (m * r) is ext-real V31() real set
(m * r) " is ext-real V31() real set
(k * s) * ((m * r) ") is ext-real V31() real set
p + q is ext-real V31() real set
r is ext-real V31() real integer () set
s is ext-real V31() real integer () set
s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set
m is ext-real V31() real integer () set
k is ext-real V31() real integer () set
k / m is ext-real V31() real set
m " is ext-real V31() real set
k * (m ") is ext-real V31() real set
k * r is ext-real V31() real integer () set
s * m is ext-real V31() real integer () set
(k * r) + (s * m) is ext-real V31() real integer () set
m * r is ext-real V31() real integer () set
((k * r) + (s * m)) / (m * r) is ext-real V31() real set
(m * r) " is ext-real V31() real set
((k * r) + (s * m)) * ((m * r) ") is ext-real V31() real set
p - q is ext-real V31() real set
- q is ext-real V31() real set
p + (- q) is ext-real V31() real set
r is ext-real V31() real integer () set
s is ext-real V31() real integer () set
s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set
m is ext-real V31() real integer () set
k is ext-real V31() real integer () set
k / m is ext-real V31() real set
m " is ext-real V31() real set
k * (m ") is ext-real V31() real set
k * r is ext-real V31() real integer () set
s * m is ext-real V31() real integer () set
(k * r) - (s * m) is ext-real V31() real integer () set
- (s * m) is ext-real V31() real integer () set
(k * r) + (- (s * m)) is ext-real V31() real integer () set
m * r is ext-real V31() real integer () set
((k * r) - (s * m)) / (m * r) is ext-real V31() real set
(m * r) " is ext-real V31() real set
((k * r) - (s * m)) * ((m * r) ") is ext-real V31() real set
p / q is ext-real V31() real set
q " is ext-real V31() real set
p * (q ") is ext-real V31() real set
r is ext-real V31() real integer () set
s is ext-real V31() real integer () set
s / r is ext-real V31() real set
r " is ext-real V31() real set
s * (r ") is ext-real V31() real set
m is ext-real V31() real integer () set
k is ext-real V31() real integer () set
k / m is ext-real V31() real set
m " is ext-real V31() real set
k * (m ") is ext-real V31() real set
1 / (k / m) is ext-real V31() real Element of REAL
(k / m) " is ext-real V31() real set
1 * ((k / m) ") is ext-real V31() real set
p * (1 / (k / m)) is ext-real V31() real Element of REAL
1 * m is ext-real V31() real integer () Element of REAL
(1 * m) / k is ext-real V31() real Element of REAL
k " is ext-real V31() real set
(1 * m) * (k ") is ext-real V31() real set
p * ((1 * m) / k) is ext-real V31() real Element of REAL
s * m is ext-real V31() real integer () set
r * k is ext-real V31() real integer () set
(s * m) / (r * k) is ext-real V31() real set
(r * k) " is ext-real V31() real set
(s * m) * ((r * k) ") is ext-real V31() real set
p is ext-real V31() real () set
- p is ext-real V31() real set
s is ext-real V31() real integer () set
q is ext-real V31() real integer () set
q / s is ext-real V31() real () set
s " is ext-real V31() real set
q * (s ") is ext-real V31() real set
- q is ext-real V31() real integer () set
(- q) / s is ext-real V31() real () set
(- q) * (s ") is ext-real V31() real set
p " is ext-real V31() real set
1 / p is ext-real V31() real () Element of REAL
1 * (p ") is ext-real V31() real set
p is ext-real V31() real set
q is ext-real V31() real set
q - p is ext-real V31() real set
- p is ext-real V31() real set
q + (- p) is ext-real V31() real set
(q - p) " is ext-real V31() real set
[\((q - p) ")/] is ext-real V31() real integer () set
[\((q - p) ")/] + 1 is ext-real V31() real integer () Element of REAL
([\((q - p) ")/] + 1) * p is ext-real V31() real Element of REAL
[\(([\((q - p) ")/] + 1) * p)/] is ext-real V31() real integer () set
[\(([\((q - p) ")/] + 1) * p)/] + 1 is ext-real V31() real integer () Element of REAL
([\(([\((q - p) ")/] + 1) * p)/] + 1) / ([\((q - p) ")/] + 1) is ext-real V31() real () Element of REAL
([\((q - p) ")/] + 1) " is ext-real V31() real () set
([\(([\((q - p) ")/] + 1) * p)/] + 1) * (([\((q - p) ")/] + 1) ") is ext-real V31() real () set
p - p is ext-real V31() real set
p + (- p) is ext-real V31() real set
((q - p) ") - 1 is ext-real V31() real Element of REAL
- 1 is ext-real non positive V31() real integer () set
((q - p) ") + (- 1) is ext-real V31() real set
([\((q - p) ")/] + 1) * (q - p) is ext-real V31() real Element of REAL
((q - p) ") * (q - p) is ext-real V31() real set
(([\((q - p) ")/] + 1) * p) - 1 is ext-real V31() real Element of REAL
(([\((q - p) ")/] + 1) * p) + (- 1) is ext-real V31() real set
([\((q - p) ")/] + 1) " is ext-real V31() real () Element of REAL
(([\((q - p) ")/] + 1) ") * ([\(([\((q - p) ")/] + 1) * p)/] + 1) is ext-real V31() real () Element of REAL
(([\((q - p) ")/] + 1) ") * (([\((q - p) ")/] + 1) * p) is ext-real V31() real Element of REAL
(([\((q - p) ")/] + 1) ") * ([\((q - p) ")/] + 1) is ext-real V31() real () Element of REAL
((([\((q - p) ")/] + 1) ") * ([\((q - p) ")/] + 1)) * p is ext-real V31() real Element of REAL
1 * p is ext-real V31() real Element of REAL
(([\((q - p) ")/] + 1) * p) + (([\((q - p) ")/] + 1) * (q - p)) is ext-real V31() real Element of REAL
([\((q - p) ")/] + 1) * q is ext-real V31() real Element of REAL
(([\((q - p) ")/] + 1) ") * (([\((q - p) ")/] + 1) * q) is ext-real V31() real Element of REAL
((([\((q - p) ")/] + 1) ") * ([\((q - p) ")/] + 1)) * q is ext-real V31() real Element of REAL
1 * q is ext-real V31() real Element of REAL
p is ext-real V31() real () set
s is ext-real V31() real integer () set
q is ext-real V31() real integer () set
q / s is ext-real V31() real () set
s " is ext-real V31() real () set
q * (s ") is ext-real V31() real () set
- q is ext-real V31() real integer () set
(- q) / s is ext-real V31() real () set
(- q) * (s ") is ext-real V31() real () set
- ((- q) / s) is ext-real V31() real () set
- s is ext-real V31() real integer () set
(- q) / (- s) is ext-real V31() real () set
(- s) " is ext-real V31() real () set
(- q) * ((- s) ") is ext-real V31() real () set
p is ext-real V31() real () set

q is ext-real V31() real integer () set
q / s is ext-real V31() real () Element of REAL
s " is ext-real non negative V31() real () set
q * (s ") is ext-real V31() real () set

s is ext-real V31() real integer () set
s / q is ext-real V31() real () set
q " is ext-real non negative V31() real () set
s * (q ") is ext-real V31() real () set

r is ext-real V31() real integer () set
r / q is ext-real V31() real () set
q " is ext-real non negative V31() real () set
r * (q ") is ext-real V31() real () set
r is ext-real V31() real integer () set
r / s is ext-real V31() real () Element of REAL
s " is ext-real non negative V31() real () set
r * (s ") is ext-real V31() real () set

k is ext-real V31() real integer () set
k / m is ext-real V31() real () Element of REAL
m " is ext-real non negative V31() real () set
k * (m ") is ext-real V31() real () set
p is ext-real V31() real () set

q is ext-real V31() real integer () set
q / s is ext-real V31() real () Element of REAL
s " is ext-real non negative V31() real () set
q * (s ") is ext-real V31() real () set

r is ext-real V31() real integer () set
r / k is ext-real V31() real () Element of REAL
k " is ext-real non negative V31() real () set
r * (k ") is ext-real V31() real () set

r is ext-real V31() real integer () set
r / q is ext-real V31() real () Element of REAL
q " is ext-real non negative V31() real () set
r * (q ") is ext-real V31() real () set
r is ext-real V31() real integer () set
r / s is ext-real V31() real () Element of REAL
s " is ext-real non negative V31() real () set
r * (s ") is ext-real V31() real () set
p is ext-real V31() real () set

(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real integer () set
q / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
q * ((p) ") is ext-real V31() real () set
p is ext-real V31() real () set

p is ext-real V31() real () set

p is ext-real V31() real () set

(p) " is ext-real non negative V31() real () Element of REAL
p is ext-real V31() real () set

(p) " is ext-real non negative V31() real () Element of REAL
1 * ((p) ") is ext-real non negative V31() real () Element of REAL
(p) * ((p) ") is ext-real non negative V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
(p) " is ext-real non negative V31() real () Element of REAL
(p) * ((p) ") is ext-real V31() real () Element of REAL
((p) ") * (p) is ext-real V31() real () Element of REAL
(p) * ((p) ") is ext-real non negative V31() real () Element of REAL
p * ((p) * ((p) ")) is ext-real V31() real () Element of REAL
p * 1 is ext-real V31() real () Element of REAL
p is ext-real V31() real () set

(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
(p) / p is ext-real V31() real () set
p " is ext-real V31() real () set
(p) * (p ") is ext-real V31() real () set
(p ") * p is ext-real V31() real () set
((p ") * p) * (p) is ext-real V31() real () Element of REAL
(p ") * (p) is ext-real V31() real () set

p is ext-real V31() real () set

(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real integer () set
q / 1 is ext-real V31() real () Element of REAL
1 " is non empty ext-real positive non negative V31() real () set
q * (1 ") is ext-real V31() real () set
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real () set

(q) is ext-real V31() real integer () set
(q) * q is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
p is ext-real V31() real () set

1 " is non empty ext-real positive non negative V31() real () Element of REAL
p is ext-real V31() real () set

(p) " is ext-real non negative V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
- 1 is ext-real non positive V31() real integer () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real non positive V31() real integer () Element of REAL
(- (p)) / (p) is ext-real non positive V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(- (p)) * ((p) ") is ext-real non positive V31() real () set
(p) / (p) is ext-real non negative V31() real () Element of REAL
(p) * ((p) ") is ext-real non negative V31() real () set
- ((p) / (p)) is ext-real non positive V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real V31() real integer () set
- (p) is ext-real non positive V31() real integer () Element of REAL
p is ext-real V31() real integer () set
q is ext-real V31() real () set
(q) is ext-real V31() real integer () set

(q) * q is ext-real V31() real () Element of REAL
(q) * p is ext-real V31() real integer () set
(q) * p is ext-real V31() real integer () Element of REAL
((q) * p) / ((q) * p) is ext-real V31() real () Element of REAL
((q) * p) " is ext-real V31() real () set
((q) * p) * (((q) * p) ") is ext-real V31() real () set
(q) / (q) is ext-real V31() real () Element of REAL
(q) " is ext-real non negative V31() real () set
(q) * ((q) ") is ext-real V31() real () set

q is ext-real V31() real integer () set
q / p is ext-real V31() real () Element of REAL
p " is ext-real non negative V31() real () set
q * (p ") is ext-real V31() real () set
s is ext-real V31() real () set
(s) is ext-real V31() real integer () set

(s) * s is ext-real V31() real () Element of REAL
s * p is ext-real V31() real () Element of REAL

(s) * k is ext-real V31() real integer () Element of REAL

p - (k * (s)) is ext-real V31() real integer () Element of REAL
- (k * (s)) is ext-real non positive V31() real integer () set
p + (- (k * (s))) is ext-real V31() real integer () set

((s) * k) / (k * (s)) is ext-real V31() real () Element of REAL
(k * (s)) " is ext-real non negative V31() real () set
((s) * k) * ((k * (s)) ") is ext-real V31() real () set
q - ((s) * k) is ext-real V31() real integer () Element of REAL
- ((s) * k) is ext-real V31() real integer () set
q + (- ((s) * k)) is ext-real V31() real integer () set
(q - ((s) * k)) / m is ext-real V31() real () Element of REAL
m " is ext-real non negative V31() real () set
(q - ((s) * k)) * (m ") is ext-real V31() real () set
(k * (s)) + (1 * (s)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real integer () Element of NAT

(s) / (s) is ext-real V31() real () Element of REAL
(s) " is ext-real non negative V31() real () set
(s) * ((s) ") is ext-real V31() real () set
((s) / (s)) * ((s) * k) is ext-real V31() real () Element of REAL
((s) / (s)) * (s) is ext-real V31() real () Element of REAL
(((s) / (s)) * (s)) * k is ext-real V31() real () Element of REAL
p is ext-real V31() real integer () set
q is ext-real V31() real integer () set
p / q is ext-real V31() real () set
q " is ext-real V31() real () set
p * (q ") is ext-real V31() real () set
s is ext-real V31() real () set
(s) is ext-real V31() real integer () set

(s) * s is ext-real V31() real () Element of REAL
- q is ext-real V31() real integer () set
- p is ext-real V31() real integer () set
(- p) / q is ext-real V31() real () set
(- p) * (q ") is ext-real V31() real () set
- ((- p) / q) is ext-real V31() real () set

(- p) / r is ext-real V31() real () Element of REAL
r " is ext-real non negative V31() real () set
(- p) * (r ") is ext-real V31() real () set

(s) * k is ext-real V31() real integer () Element of REAL

- k is ext-real non positive V31() real integer () Element of REAL
m is ext-real non positive V31() real integer () Element of REAL
(s) * m is ext-real V31() real integer () set
(s) * m is ext-real non positive V31() real integer () Element of REAL
- ((s) * k) is ext-real V31() real integer () Element of REAL
(s) * m is ext-real V31() real integer () Element of REAL
- ((s) * k) is ext-real non positive V31() real integer () Element of REAL

(s) * k is ext-real V31() real integer () Element of REAL

m is ext-real V31() real integer () set
(s) * m is ext-real V31() real integer () set
(s) * m is ext-real V31() real integer () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL

s is ext-real V31() real integer () set
s * q is ext-real V31() real integer () Element of REAL

s is ext-real V31() real integer () set
s * q is ext-real V31() real integer () Element of REAL

s is ext-real V31() real integer () set
s * q is ext-real V31() real integer () Element of REAL

(s * q) / (r * q) is ext-real V31() real () Element of REAL
(r * q) " is ext-real non negative V31() real () set
(s * q) * ((r * q) ") is ext-real V31() real () set
s / r is ext-real V31() real () Element of REAL
r " is ext-real non negative V31() real () set
s * (r ") is ext-real V31() real () set
q / q is ext-real non negative V31() real () Element of REAL
q " is ext-real non negative V31() real () set
q * (q ") is ext-real non negative V31() real () set
(s / r) * (q / q) is ext-real V31() real () Element of REAL
(s / r) * 1 is ext-real V31() real () Element of REAL

q is ext-real V31() real integer () set
q / p is ext-real V31() real () Element of REAL
p " is ext-real non negative V31() real () set
q * (p ") is ext-real V31() real () set
s is ext-real V31() real () set

(s) is ext-real V31() real integer () set
(s) * s is ext-real V31() real () Element of REAL

(s) * r is ext-real V31() real integer () Element of REAL

p is ext-real V31() real () set

- (p) is ext-real non positive V31() real integer () Element of REAL
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () Element of REAL
(- 1) * (p) is ext-real non positive V31() real integer () Element of REAL
((- 1) * (p)) * ((p) ") is ext-real non positive V31() real () Element of REAL
(p) * ((p) ") is ext-real V31() real () Element of REAL
(p) * ((p) ") is ext-real non negative V31() real () Element of REAL
(- 1) * ((p) * ((p) ")) is ext-real non positive V31() real () Element of REAL
(- 1) * 1 is ext-real non positive V31() real integer () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
((p) / (p)) * (p) is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real non positive V31() real integer () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real V31() real integer () set
- (p) is ext-real non positive V31() real integer () Element of REAL
- (- (p)) is ext-real V31() real integer () set
p is ext-real V31() real () set

(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real V31() real integer () set
- (- (p)) is ext-real V31() real integer () set
- (p) is ext-real non positive V31() real integer () Element of REAL
p is ext-real V31() real () set

(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () Element of REAL
(p) * ((p) ") is ext-real non negative V31() real () Element of REAL
(p) * ((p) ") is ext-real V31() real () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set

((p) / (p)) * (p) is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
p is ext-real V31() real () set
(p) is ext-real V31() real integer () set

(p) * p is ext-real V31() real () Element of REAL
p is ext-real V31() real set
q is ext-real V31() real () set
(q) is ext-real V31() real integer () set

(q) * q is ext-real V31() real () Element of REAL
p * (q) is ext-real V31() real Element of REAL
(q) " is ext-real non negative V31() real () Element of REAL
(q) * ((q) ") is ext-real V31() real () Element of REAL
(p * (q)) * ((q) ") is ext-real V31() real Element of REAL
(q) * ((q) ") is ext-real non negative V31() real () Element of REAL
p * ((q) * ((q) ")) is ext-real V31() real Element of REAL
p * 1 is ext-real V31() real Element of REAL
p is ext-real V31() real set
q is ext-real V31() real () set

p * (q) is ext-real V31() real Element of REAL
(q) is ext-real V31() real integer () set
(q) * q is ext-real V31() real () Element of REAL

(p * (q)) / (1 * (q)) is ext-real V31() real Element of REAL
(1 * (q)) " is ext-real non negative V31() real () set
(p * (q)) * ((1 * (q)) ") is ext-real V31() real set
p / 1 is ext-real V31() real Element of REAL
1 " is non empty ext-real positive non negative V31() real () set
p * (1 ") is ext-real V31() real set
(q) / (q) is ext-real non negative V31() real () Element of REAL
(q) " is ext-real non negative V31() real () set
(q) * ((q) ") is ext-real non negative V31() real () set
(p / 1) * ((q) / (q)) is ext-real V31() real Element of REAL
p is ext-real V31() real () set

(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real () set

(q) is ext-real V31() real integer () set
(q) * q is ext-real V31() real () Element of REAL
(q) / (q) is ext-real V31() real () Element of REAL
(q) " is ext-real non negative V31() real () set
(q) * ((q) ") is ext-real V31() real () set
p is ext-real V31() real () set

(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real () set
(q) is ext-real V31() real integer () set

(q) * q is ext-real V31() real () Element of REAL
(q) * (p) is ext-real V31() real integer () Element of REAL
(p) * (q) is ext-real V31() real integer () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
(q) / (q) is ext-real V31() real () Element of REAL
(q) " is ext-real non negative V31() real () set
(q) * ((q) ") is ext-real V31() real () set
p is ext-real V31() real () set
- p is ext-real V31() real () set

((- p)) is ext-real V31() real integer () set
((- p)) * (- p) is ext-real V31() real () Element of REAL
(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
- (p) is ext-real V31() real integer () set
- (- p) is ext-real V31() real () set
((- p)) / ((- p)) is ext-real V31() real () Element of REAL
((- p)) " is ext-real non negative V31() real () set
((- p)) * (((- p)) ") is ext-real V31() real () set
- (((- p)) / ((- p))) is ext-real V31() real () Element of REAL
- ((- p)) is ext-real V31() real integer () set
(- ((- p))) / ((- p)) is ext-real V31() real () Element of REAL
(- ((- p))) * (((- p)) ") is ext-real V31() real () set

(p) * q is ext-real V31() real integer () Element of REAL

(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
- ((p) / (p)) is ext-real V31() real () Element of REAL
(- (p)) / (p) is ext-real V31() real () Element of REAL
(- (p)) * ((p) ") is ext-real V31() real () set

((- p)) * s is ext-real V31() real integer () Element of REAL

p is ext-real V31() real () set
1 / p is ext-real V31() real () Element of REAL
p " is ext-real V31() real () set
1 * (p ") is ext-real V31() real () set

(p) is ext-real V31() real integer () set
(p) * p is ext-real V31() real () Element of REAL
q is ext-real V31() real () set
(q) is ext-real V31() real integer () set

(q) * q is ext-real V31() real () Element of REAL
(p) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real non negative V31() real () set
(p) * ((p) ") is ext-real V31() real () set
1 / ((p) / (p)) is ext-real V31() real () Element of REAL
((p) / (p)) " is ext-real V31() real () set
1 * (((p) / (p)) ") is ext-real V31() real () set

(1 * (p)) / (p) is ext-real V31() real () Element of REAL
(p) " is ext-real V31() real () set
(1 * (p)) * ((p) ") is ext-real V31() real () set
(p) / (p) is ext-real V31() real () Element of REAL
(p) * ((p) ") is ext-real V31() real () set

m is ext-real V31() real integer () set
m * k is ext-real V31() real integer () Element of REAL

m is ext-real V31() real integer () set
m * k is ext-real V31() real integer () Element of REAL

m is ext-real V31() real integer () set
m * k is ext-real V31() real integer () Element of REAL

0 * m is ext-real V31() real integer () Element of REAL

p is ext-real V31() real () set
1 / p is ext-r