:: NUMBERS semantic presentation

omega is non empty epsilon-transitive epsilon-connected ordinal non finite set
RAT+ is non empty set
{} is Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite set
the Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite set is Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite Element of omega
{ [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : verum } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : verum } is Element of bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) }
bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
( { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : verum } ) \/ omega is non empty set
bool RAT+ is set
bool (bool RAT+) is set
DEDEKIND_CUTS is non empty Element of bool (bool RAT+)
REAL+ is non empty set
{ b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } is set
{RAT+} is non empty set
{ b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } \ {RAT+} is Element of bool { b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) }
bool { b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } is set
RAT+ \/ DEDEKIND_CUTS is non empty set
{} is Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite Element of RAT+
{ { b₂ where b₂ is Element of RAT+ : not b₁ <=' b₂ } where b₁ is Element of RAT+ : not b₁ = {} } is set
(RAT+ \/ DEDEKIND_CUTS) \ { { b₂ where b₂ is Element of RAT+ : not b₁ <=' b₂ } where b₁ is Element of RAT+ : not b₁ = {} } is Element of bool (RAT+ \/ DEDEKIND_CUTS)
bool (RAT+ \/ DEDEKIND_CUTS) is set
one is non empty epsilon-transitive epsilon-connected ordinal natural finite Element of RAT+
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : verum } is Element of bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) }
bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
( { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : verum } ) \/ omega is non empty set
succ {} is non empty epsilon-transitive epsilon-connected ordinal natural finite set
{{}} is non empty set
[:{{}},REAL+:] is Relation-like set
REAL+ \/ [:{{}},REAL+:] is non empty set
[{},{}] is V15() set
{{},{}} is non empty set
{{{},{}},{{}}} is non empty set
{[{},{}]} is Relation-like non empty set
(REAL+ \/ [:{{}},REAL+:]) \ {[{},{}]} is Element of bool (REAL+ \/ [:{{}},REAL+:])
bool (REAL+ \/ [:{{}},REAL+:]) is set
() is set
{{},1} is non empty set
Funcs ({{},1},()) is functional non empty FUNCTION_DOMAIN of {{},1},()
{ b₁ where b₁ is Relation-like Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},()) : b₁ . 1 = {} } is set
(Funcs ({{},1},())) \ { b₁ where b₁ is Relation-like Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},()) : b₁ . 1 = {} } is Element of bool (Funcs ({{},1},()))
bool (Funcs ({{},1},())) is set
((Funcs ({{},1},())) \ { b₁ where b₁ is Relation-like Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},()) : b₁ . 1 = {} } ) \/ () is non empty set
[:{{}},RAT+:] is Relation-like set
RAT+ \/ [:{{}},RAT+:] is non empty set
(RAT+ \/ [:{{}},RAT+:]) \ {[{},{}]} is Element of bool (RAT+ \/ [:{{}},RAT+:])
bool (RAT+ \/ [:{{}},RAT+:]) is set
[:{{}},omega:] is Relation-like non finite set
omega \/ [:{{}},omega:] is non empty set
(omega \/ [:{{}},omega:]) \ {[{},{}]} is Element of bool (omega \/ [:{{}},omega:])
bool (omega \/ [:{{}},omega:]) is set
bool () is set
() is set
() is set
() is set
() is non empty epsilon-transitive epsilon-connected ordinal non finite Element of bool ()
[:{{}},():] is Relation-like non finite set
() \/ [:{{}},():] is non empty set
a9 is set
two is set
[a9,two] is V15() set
{a9,two} is non empty set
{a9} is non empty set
{{a9,two},{a9}} is non empty set
c is set
{c} is non empty set
a9 is Element of ()
two is Element of ()
({},one) --> (a9,two) is Relation-like Function-like non empty V14({{},one}) quasi_total Element of bool [:{{},one},():]
{{},one} is non empty set
[:{{},one},():] is Relation-like set
bool [:{{},one},():] is set
[{},a9] is V15() set
{{},a9} is non empty set
{{{},a9},{{}}} is non empty set
[one,two] is V15() set
{one,two} is non empty set
{one} is non empty set
{{one,two},{one}} is non empty set
{[{},a9],[one,two]} is Relation-like non empty set
{{}} is non empty set
[:{{}},REAL+:] is Relation-like set
d2 is set
DD is set
[d2,DD] is V15() set
{d2,DD} is non empty set
{d2} is non empty set
{{d2,DD},{d2}} is non empty set
{{},DD} is non empty set
{{},DD} is non empty set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of () : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
d2 is epsilon-transitive epsilon-connected ordinal natural finite Element of ()
DD is epsilon-transitive epsilon-connected ordinal natural finite Element of ()
[d2,DD] is V15() set
{d2,DD} is non empty set
{d2} is non empty set
{{d2,DD},{d2}} is non empty set
{{d2}} is non empty set
{ [b₁,one] where b₁ is epsilon-transitive epsilon-connected ordinal natural finite Element of () : verum } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of () : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,one] where b₁ is epsilon-transitive epsilon-connected ordinal natural finite Element of () : verum } is Element of bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of () : ( b₁,b₂ are_relative_prime & not b₂ = {} ) }
bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of () : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
d2 is set
[{},d2] is V15() set
{{},d2} is non empty set
{{{},d2},{{}}} is non empty set
DD is set
[one,DD] is V15() set
{one,DD} is non empty set
{{one,DD},{one}} is non empty set
{[{},d2],[one,DD]} is Relation-like non empty set
half is Element of bool RAT+
r is Element of RAT+
3r9 is Element of RAT+
r is Element of RAT+
3r9 is Element of RAT+
rr is Element of RAT+
() is Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite Element of ()
{(),one} is non empty set
Funcs ({(),one},()) is functional non empty FUNCTION_DOMAIN of {(),one},()
{ b₁ where b₁ is Relation-like Function-like V14({(),one}) quasi_total Element of Funcs ({(),one},()) : b₁ . one = () } is set
((),1) --> ((),1) is Relation-like Function-like non empty V14({(),1}) quasi_total Element of bool [:{(),1},omega:]
{(),1} is non empty set
[:{(),1},omega:] is Relation-like non finite set
bool [:{(),1},omega:] is non finite set
two is Relation-like Function-like V14({(),one}) quasi_total Element of Funcs ({(),one},())
two . one is set
{{}} is non empty set
[:{{}},REAL+:] is Relation-like set
REAL+ \/ [:{{}},REAL+:] is non empty set
two is Element of ()
c is Element of ()
((),1) --> (two,c) is Relation-like Function-like non empty V14({(),1}) quasi_total Element of bool [:{(),1},():]
[:{(),1},():] is Relation-like set
bool [:{(),1},():] is set
rng (((),1) --> ((),1)) is non empty set
dom (((),1) --> ((),1)) is non empty set
(Funcs ({(),one},())) \ { b₁ where b₁ is Relation-like Function-like V14({(),one}) quasi_total Element of Funcs ({(),one},()) : b₁ . one = () } is Element of bool (Funcs ({(),one},()))
bool (Funcs ({(),one},())) is set
() is Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite Element of ()
{()} is non empty set
[:{()},RAT+:] is Relation-like set
[:{()},REAL+:] is Relation-like set
RAT+ \/ [:{()},RAT+:] is non empty set
REAL+ \/ [:{()},REAL+:] is non empty set
a9 is epsilon-transitive epsilon-connected ordinal natural finite Element of RAT+
two is epsilon-transitive epsilon-connected ordinal natural finite Element of RAT+
c is Element of REAL+
d1 is Element of REAL+
d2 is Element of RAT+
DD is Element of RAT+
a9 is epsilon-transitive epsilon-connected ordinal natural finite Element of RAT+
two is epsilon-transitive epsilon-connected ordinal natural finite Element of RAT+
c is epsilon-transitive epsilon-connected ordinal set
a9 +^ c is epsilon-transitive epsilon-connected ordinal set
d1 is Element of RAT+
a9 + d1 is Element of RAT+
numerator a9 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator d1 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator a9) *^ (denominator d1) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator d1 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator a9 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator d1) *^ (denominator a9) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator a9) *^ (denominator d1)) +^ ((numerator d1) *^ (denominator a9)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator a9) *^ (denominator d1) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator a9) *^ (denominator d1)) +^ ((numerator d1) *^ (denominator a9))) / ((denominator a9) *^ (denominator d1)) is Element of RAT+
2 is non empty epsilon-transitive epsilon-connected ordinal natural finite Element of omega
succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite set
() is Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite Element of ()
succ () is non empty epsilon-transitive epsilon-connected ordinal natural finite set
{1} is non empty set
(succ ()) \/ {1} is non empty set
{()} is non empty set
() \/ {()} is non empty set
(() \/ {()}) \/ {1} is non empty set
{(),1} is non empty set
a9 is epsilon-transitive epsilon-connected ordinal natural finite set
a9 *^ a9 is epsilon-transitive epsilon-connected ordinal natural finite set
two is epsilon-transitive epsilon-connected ordinal natural finite set
2 *^ two is epsilon-transitive epsilon-connected ordinal natural finite set
a9 div^ 2 is epsilon-transitive epsilon-connected ordinal natural finite set
a9 mod^ 2 is epsilon-transitive epsilon-connected ordinal natural finite set
d1 is epsilon-transitive epsilon-connected ordinal natural finite set
2 *^ d1 is epsilon-transitive epsilon-connected ordinal natural finite set
d1 *^ 2 is epsilon-transitive epsilon-connected ordinal natural finite set
(d1 *^ 2) +^ () is epsilon-transitive epsilon-connected ordinal natural finite set
(a9 div^ 2) *^ 2 is epsilon-transitive epsilon-connected ordinal natural finite set
((a9 div^ 2) *^ 2) +^ 1 is epsilon-transitive epsilon-connected ordinal natural finite set
((a9 div^ 2) *^ 2) *^ (((a9 div^ 2) *^ 2) +^ 1) is epsilon-transitive epsilon-connected ordinal natural finite set
one *^ (((a9 div^ 2) *^ 2) +^ 1) is epsilon-transitive epsilon-connected ordinal natural finite set
(((a9 div^ 2) *^ 2) *^ (((a9 div^ 2) *^ 2) +^ 1)) +^ (one *^ (((a9 div^ 2) *^ 2) +^ 1)) is epsilon-transitive epsilon-connected ordinal natural finite set
one *^ ((a9 div^ 2) *^ 2) is epsilon-transitive epsilon-connected ordinal natural finite set
one *^ 1 is epsilon-transitive epsilon-connected ordinal natural finite set
(one *^ ((a9 div^ 2) *^ 2)) +^ (one *^ 1) is epsilon-transitive epsilon-connected ordinal natural finite set
(((a9 div^ 2) *^ 2) *^ (((a9 div^ 2) *^ 2) +^ 1)) +^ ((one *^ ((a9 div^ 2) *^ 2)) +^ (one *^ 1)) is epsilon-transitive epsilon-connected ordinal natural finite set
(one *^ ((a9 div^ 2) *^ 2)) +^ 1 is epsilon-transitive epsilon-connected ordinal natural finite set
(((a9 div^ 2) *^ 2) *^ (((a9 div^ 2) *^ 2) +^ 1)) +^ ((one *^ ((a9 div^ 2) *^ 2)) +^ 1) is epsilon-transitive epsilon-connected ordinal natural finite set
(((a9 div^ 2) *^ 2) *^ (((a9 div^ 2) *^ 2) +^ 1)) +^ (one *^ ((a9 div^ 2) *^ 2)) is epsilon-transitive epsilon-connected ordinal natural finite set
((((a9 div^ 2) *^ 2) *^ (((a9 div^ 2) *^ 2) +^ 1)) +^ (one *^ ((a9 div^ 2) *^ 2))) +^ 1 is epsilon-transitive epsilon-connected ordinal natural finite set
(((a9 div^ 2) *^ 2) +^ 1) +^ one is epsilon-transitive epsilon-connected ordinal natural finite set
((a9 div^ 2) *^ 2) *^ ((((a9 div^ 2) *^ 2) +^ 1) +^ one) is epsilon-transitive epsilon-connected ordinal natural finite set
(((a9 div^ 2) *^ 2) *^ ((((a9 div^ 2) *^ 2) +^ 1) +^ one)) +^ 1 is epsilon-transitive epsilon-connected ordinal natural finite set
(a9 div^ 2) *^ ((((a9 div^ 2) *^ 2) +^ 1) +^ one) is epsilon-transitive epsilon-connected ordinal natural finite set
((a9 div^ 2) *^ ((((a9 div^ 2) *^ 2) +^ 1) +^ one)) *^ 2 is epsilon-transitive epsilon-connected ordinal natural finite set
(((a9 div^ 2) *^ ((((a9 div^ 2) *^ 2) +^ 1) +^ one)) *^ 2) +^ 1 is epsilon-transitive epsilon-connected ordinal natural finite set
one + one is Element of RAT+
numerator one is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator one is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator one) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator one) *^ (denominator one)) +^ ((numerator one) *^ (denominator one)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator one) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator one) *^ (denominator one)) +^ ((numerator one) *^ (denominator one))) / ((denominator one) *^ (denominator one)) is Element of RAT+
two is epsilon-transitive epsilon-connected ordinal natural finite Element of RAT+
1 +^ 1 is epsilon-transitive epsilon-connected ordinal natural finite set
1 +^ {} is epsilon-transitive epsilon-connected ordinal natural finite set
succ (1 +^ {}) is non empty epsilon-transitive epsilon-connected ordinal natural finite set
c is Element of RAT+
c + c is Element of RAT+
numerator c is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator c is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator c) *^ (denominator c) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator c) *^ (denominator c)) +^ ((numerator c) *^ (denominator c)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator c) *^ (denominator c) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator c) *^ (denominator c)) +^ ((numerator c) *^ (denominator c))) / ((denominator c) *^ (denominator c)) is Element of RAT+
two *' c is Element of RAT+
numerator two is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator two) *^ (numerator c) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator two is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator two) *^ (denominator c) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (numerator c)) / ((denominator two) *^ (denominator c)) is Element of RAT+
one *' c is Element of RAT+
(numerator one) *^ (numerator c) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator one) *^ (denominator c) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator one) *^ (numerator c)) / ((denominator one) *^ (denominator c)) is Element of RAT+
(one *' c) + c is Element of RAT+
numerator (one *' c) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (one *' c)) *^ (denominator c) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (one *' c) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator c) *^ (denominator (one *' c)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (one *' c)) *^ (denominator c)) +^ ((numerator c) *^ (denominator (one *' c))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (one *' c)) *^ (denominator c) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (one *' c)) *^ (denominator c)) +^ ((numerator c) *^ (denominator (one *' c)))) / ((denominator (one *' c)) *^ (denominator c)) is Element of RAT+
(one *' c) + (one *' c) is Element of RAT+
(numerator (one *' c)) *^ (denominator (one *' c)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (one *' c)) *^ (denominator (one *' c))) +^ ((numerator (one *' c)) *^ (denominator (one *' c))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (one *' c)) *^ (denominator (one *' c)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (one *' c)) *^ (denominator (one *' c))) +^ ((numerator (one *' c)) *^ (denominator (one *' c)))) / ((denominator (one *' c)) *^ (denominator (one *' c))) is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : S₁[b₁] } is set
2 *^ 2 is epsilon-transitive epsilon-connected ordinal natural finite set
two *' two is Element of RAT+
numerator two is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator two) *^ (numerator two) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator two is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator two) *^ (denominator two) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (numerator two)) / ((denominator two) *^ (denominator two)) is Element of RAT+
1 *^ 2 is epsilon-transitive epsilon-connected ordinal natural finite set
1 \/ {1} is non empty set
a9 is Element of RAT+
a9 *' a9 is Element of RAT+
numerator a9 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator a9) *^ (numerator a9) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator a9 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator a9) *^ (denominator a9) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator a9) *^ (numerator a9)) / ((denominator a9) *^ (denominator a9)) is Element of RAT+
d1 is Element of bool RAT+
d2 is Element of RAT+
DD is Element of RAT+
DD *' DD is Element of RAT+
numerator DD is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator DD) *^ (numerator DD) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator DD is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator DD) *^ (denominator DD) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator DD) *^ (numerator DD)) / ((denominator DD) *^ (denominator DD)) is Element of RAT+
DD *' d2 is Element of RAT+
numerator d2 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator DD) *^ (numerator d2) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator d2 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator DD) *^ (denominator d2) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator DD) *^ (numerator d2)) / ((denominator DD) *^ (denominator d2)) is Element of RAT+
d2 *' d2 is Element of RAT+
(numerator d2) *^ (numerator d2) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator d2) *^ (denominator d2) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator d2) *^ (numerator d2)) / ((denominator d2) *^ (denominator d2)) is Element of RAT+
half is Element of RAT+
half *' half is Element of RAT+
numerator half is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator half) *^ (numerator half) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator half is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator half) *^ (denominator half) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator half) *^ (numerator half)) / ((denominator half) *^ (denominator half)) is Element of RAT+
[(),()] is V15() set
{(),()} is non empty set
{{(),()},{()}} is non empty set
{{()},{()}} is non empty set
{{()}} is non empty set
{[(),()]} is Relation-like non empty set
half is Element of RAT+
two *' half is Element of RAT+
numerator half is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator two) *^ (numerator half) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator half is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator two) *^ (denominator half) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (numerator half)) / ((denominator two) *^ (denominator half)) is Element of RAT+
{ { b₂ where b₂ is Element of RAT+ : not b₁ <=' b₂ } where b₁ is Element of RAT+ : not b₁ = () } is set
r is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not r <=' b₁ } is set
numerator r is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator r is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
r *' r is Element of RAT+
(numerator r) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator r)) / ((denominator r) *^ (denominator r)) is Element of RAT+
eps is Element of RAT+
eps is Element of RAT+
two + eps is Element of RAT+
denominator eps is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator two) *^ (denominator eps) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator eps is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator eps) *^ (denominator two) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (denominator eps)) +^ ((numerator eps) *^ (denominator two)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator two) *^ (denominator eps) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator two) *^ (denominator eps)) +^ ((numerator eps) *^ (denominator two))) / ((denominator two) *^ (denominator eps)) is Element of RAT+
(r *' r) + eps is Element of RAT+
numerator (r *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' r)) *^ (denominator eps) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (r *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator eps) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' r)) *^ (denominator eps)) +^ ((numerator eps) *^ (denominator (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' r)) *^ (denominator eps) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' r)) *^ (denominator eps)) +^ ((numerator eps) *^ (denominator (r *' r)))) / ((denominator (r *' r)) *^ (denominator eps)) is Element of RAT+
d2 is Element of RAT+
t is Element of RAT+
t *' one is Element of RAT+
numerator t is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator t) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator t is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator t) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator t) *^ (numerator one)) / ((denominator t) *^ (denominator one)) is Element of RAT+
t *' t is Element of RAT+
(numerator t) *^ (numerator t) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator t) *^ (denominator t) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator t) *^ (numerator t)) / ((denominator t) *^ (denominator t)) is Element of RAT+
r *' one is Element of RAT+
(numerator r) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator one)) / ((denominator r) *^ (denominator one)) is Element of RAT+
one *' r is Element of RAT+
(numerator one) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator one) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator one) *^ (numerator r)) / ((denominator one) *^ (denominator r)) is Element of RAT+
one *' one is Element of RAT+
(numerator one) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator one) *^ (numerator one)) / ((denominator one) *^ (denominator one)) is Element of RAT+
two *' r is Element of RAT+
(numerator two) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator two) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (numerator r)) / ((denominator two) *^ (denominator r)) is Element of RAT+
s is Element of RAT+
(t *' t) + s is Element of RAT+
numerator (t *' t) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator s is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (t *' t)) *^ (denominator s) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator s is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator (t *' t) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator s) *^ (denominator (t *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (t *' t)) *^ (denominator s)) +^ ((numerator s) *^ (denominator (t *' t))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (t *' t)) *^ (denominator s) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (t *' t)) *^ (denominator s)) +^ ((numerator s) *^ (denominator (t *' t)))) / ((denominator (t *' t)) *^ (denominator s)) is Element of RAT+
(r *' r) + s is Element of RAT+
(numerator (r *' r)) *^ (denominator s) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator s) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' r)) *^ (denominator s)) +^ ((numerator s) *^ (denominator (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' r)) *^ (denominator s) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' r)) *^ (denominator s)) +^ ((numerator s) *^ (denominator (r *' r)))) / ((denominator (r *' r)) *^ (denominator s)) is Element of RAT+
t02s2 is Element of RAT+
(two *' r) *' t02s2 is Element of RAT+
numerator (two *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
numerator t02s2 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (two *' r)) *^ (numerator t02s2) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (two *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator t02s2 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator (two *' r)) *^ (denominator t02s2) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (two *' r)) *^ (numerator t02s2)) / ((denominator (two *' r)) *^ (denominator t02s2)) is Element of RAT+
(t *' t) *' t02s2 is Element of RAT+
(numerator (t *' t)) *^ (numerator t02s2) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (t *' t)) *^ (denominator t02s2) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (t *' t)) *^ (numerator t02s2)) / ((denominator (t *' t)) *^ (denominator t02s2)) is Element of RAT+
x is Element of RAT+
((t *' t) *' t02s2) + x is Element of RAT+
numerator ((t *' t) *' t02s2) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator x is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((t *' t) *' t02s2)) *^ (denominator x) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator x is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator ((t *' t) *' t02s2) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator x) *^ (denominator ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t *' t) *' t02s2)) *^ (denominator x)) +^ ((numerator x) *^ (denominator ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((t *' t) *' t02s2)) *^ (denominator x) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((t *' t) *' t02s2)) *^ (denominator x)) +^ ((numerator x) *^ (denominator ((t *' t) *' t02s2)))) / ((denominator ((t *' t) *' t02s2)) *^ (denominator x)) is Element of RAT+
r + x is Element of RAT+
(numerator r) *^ (denominator x) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator x) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (denominator x)) +^ ((numerator x) *^ (denominator r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator x) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator r) *^ (denominator x)) +^ ((numerator x) *^ (denominator r))) / ((denominator r) *^ (denominator x)) is Element of RAT+
((t *' t) *' t02s2) *' (two *' r) is Element of RAT+
(numerator ((t *' t) *' t02s2)) *^ (numerator (two *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((t *' t) *' t02s2)) *^ (denominator (two *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t *' t) *' t02s2)) *^ (numerator (two *' r))) / ((denominator ((t *' t) *' t02s2)) *^ (denominator (two *' r))) is Element of RAT+
(t *' t) *' one is Element of RAT+
(numerator (t *' t)) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (t *' t)) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (t *' t)) *^ (numerator one)) / ((denominator (t *' t)) *^ (denominator one)) is Element of RAT+
((t *' t) *' t02s2) *' x is Element of RAT+
(numerator ((t *' t) *' t02s2)) *^ (numerator x) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t *' t) *' t02s2)) *^ (numerator x)) / ((denominator ((t *' t) *' t02s2)) *^ (denominator x)) is Element of RAT+
((t *' t) *' t02s2) *' r is Element of RAT+
(numerator ((t *' t) *' t02s2)) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((t *' t) *' t02s2)) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t *' t) *' t02s2)) *^ (numerator r)) / ((denominator ((t *' t) *' t02s2)) *^ (denominator r)) is Element of RAT+
(((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r) is Element of RAT+
numerator (((t *' t) *' t02s2) *' x) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator (((t *' t) *' t02s2) *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t *' t) *' t02s2) *' x)) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator (((t *' t) *' t02s2) *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator (((t *' t) *' t02s2) *' x) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((t *' t) *' t02s2) *' x)) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((t *' t) *' t02s2) *' x)) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((t *' t) *' t02s2) *' x)) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' x)))) / ((denominator (((t *' t) *' t02s2) *' x)) *^ (denominator (((t *' t) *' t02s2) *' r))) is Element of RAT+
((t *' t) *' t02s2) *' ((t *' t) *' t02s2) is Element of RAT+
(numerator ((t *' t) *' t02s2)) *^ (numerator ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((t *' t) *' t02s2)) *^ (denominator ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t *' t) *' t02s2)) *^ (numerator ((t *' t) *' t02s2))) / ((denominator ((t *' t) *' t02s2)) *^ (denominator ((t *' t) *' t02s2))) is Element of RAT+
((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r)) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)) is Element of RAT+
numerator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r))))) / ((denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is Element of RAT+
(((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)) is Element of RAT+
(numerator (((t *' t) *' t02s2) *' x)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator (((t *' t) *' t02s2) *' x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((t *' t) *' t02s2) *' x)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator (((t *' t) *' t02s2) *' x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((t *' t) *' t02s2) *' x)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((t *' t) *' t02s2) *' x)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator (((t *' t) *' t02s2) *' x)))) / ((denominator (((t *' t) *' t02s2) *' x)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is Element of RAT+
((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r) is Element of RAT+
numerator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t *' t) *' t02s2) *' r)) *^ (denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))))) / ((denominator ((((t *' t) *' t02s2) *' x) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' r))) is Element of RAT+
(((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' r) is Element of RAT+
(numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' r)))) / ((denominator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' r))) is Element of RAT+
(((t *' t) *' t02s2) *' r) *' one is Element of RAT+
(numerator (((t *' t) *' t02s2) *' r)) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((t *' t) *' t02s2) *' r)) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((t *' t) *' t02s2) *' r)) *^ (numerator one)) / ((denominator (((t *' t) *' t02s2) *' r)) *^ (denominator one)) is Element of RAT+
((((t *' t) *' t02s2) *' r) *' one) + (((t *' t) *' t02s2) *' r) is Element of RAT+
numerator ((((t *' t) *' t02s2) *' r) *' one) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((((t *' t) *' t02s2) *' r) *' one) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t *' t) *' t02s2) *' r)) *^ (denominator ((((t *' t) *' t02s2) *' r) *' one)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator ((((t *' t) *' t02s2) *' r) *' one))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator ((((t *' t) *' t02s2) *' r) *' one)))) / ((denominator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator (((t *' t) *' t02s2) *' r))) is Element of RAT+
((((t *' t) *' t02s2) *' r) *' one) + ((((t *' t) *' t02s2) *' r) *' one) is Element of RAT+
(numerator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator ((((t *' t) *' t02s2) *' r) *' one)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator ((((t *' t) *' t02s2) *' r) *' one))) +^ ((numerator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator ((((t *' t) *' t02s2) *' r) *' one))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator ((((t *' t) *' t02s2) *' r) *' one)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator ((((t *' t) *' t02s2) *' r) *' one))) +^ ((numerator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator ((((t *' t) *' t02s2) *' r) *' one)))) / ((denominator ((((t *' t) *' t02s2) *' r) *' one)) *^ (denominator ((((t *' t) *' t02s2) *' r) *' one))) is Element of RAT+
r *' ((t *' t) *' t02s2) is Element of RAT+
(numerator r) *^ (numerator ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator ((t *' t) *' t02s2))) / ((denominator r) *^ (denominator ((t *' t) *' t02s2))) is Element of RAT+
(r *' ((t *' t) *' t02s2)) *' two is Element of RAT+
numerator (r *' ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' ((t *' t) *' t02s2))) *^ (numerator two) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (r *' ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator (r *' ((t *' t) *' t02s2))) *^ (denominator two) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' ((t *' t) *' t02s2))) *^ (numerator two)) / ((denominator (r *' ((t *' t) *' t02s2))) *^ (denominator two)) is Element of RAT+
r *' two is Element of RAT+
(numerator r) *^ (numerator two) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator two) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator two)) / ((denominator r) *^ (denominator two)) is Element of RAT+
((t *' t) *' t02s2) *' (r *' two) is Element of RAT+
numerator (r *' two) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((t *' t) *' t02s2)) *^ (numerator (r *' two)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (r *' two) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator ((t *' t) *' t02s2)) *^ (denominator (r *' two)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t *' t) *' t02s2)) *^ (numerator (r *' two))) / ((denominator ((t *' t) *' t02s2)) *^ (denominator (r *' two))) is Element of RAT+
s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)) is Element of RAT+
(numerator s) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator s) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator s) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator s)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator s) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator s) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator s))) / ((denominator s) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is Element of RAT+
(s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) + (t *' t) is Element of RAT+
numerator (s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (t *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (t *' t)) *^ (denominator (s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (t *' t))) +^ ((numerator (t *' t)) *^ (denominator (s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (t *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (t *' t))) +^ ((numerator (t *' t)) *^ (denominator (s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))))) / ((denominator (s + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (t *' t))) is Element of RAT+
x + ((t *' t) *' t02s2) is Element of RAT+
((numerator x) *^ (denominator ((t *' t) *' t02s2))) +^ ((numerator ((t *' t) *' t02s2)) *^ (denominator x)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator x) *^ (denominator ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator x) *^ (denominator ((t *' t) *' t02s2))) +^ ((numerator ((t *' t) *' t02s2)) *^ (denominator x))) / ((denominator x) *^ (denominator ((t *' t) *' t02s2))) is Element of RAT+
(x + ((t *' t) *' t02s2)) *' r is Element of RAT+
numerator (x + ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (x + ((t *' t) *' t02s2))) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (x + ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator (x + ((t *' t) *' t02s2))) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (x + ((t *' t) *' t02s2))) *^ (numerator r)) / ((denominator (x + ((t *' t) *' t02s2))) *^ (denominator r)) is Element of RAT+
((x + ((t *' t) *' t02s2)) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)) is Element of RAT+
numerator ((x + ((t *' t) *' t02s2)) *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((x + ((t *' t) *' t02s2)) *' r)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((x + ((t *' t) *' t02s2)) *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator ((x + ((t *' t) *' t02s2)) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((x + ((t *' t) *' t02s2)) *' r)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator ((x + ((t *' t) *' t02s2)) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((x + ((t *' t) *' t02s2)) *' r)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((x + ((t *' t) *' t02s2)) *' r)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator ((x + ((t *' t) *' t02s2)) *' r)))) / ((denominator ((x + ((t *' t) *' t02s2)) *' r)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is Element of RAT+
x *' (x + ((t *' t) *' t02s2)) is Element of RAT+
(numerator x) *^ (numerator (x + ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator x) *^ (denominator (x + ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator x) *^ (numerator (x + ((t *' t) *' t02s2)))) / ((denominator x) *^ (denominator (x + ((t *' t) *' t02s2)))) is Element of RAT+
(x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r) is Element of RAT+
numerator (x *' (x + ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (x *' (x + ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (x *' (x + ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (x *' (x + ((t *' t) *' t02s2)))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (x *' (x + ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (x *' (x + ((t *' t) *' t02s2))))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (x *' (x + ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (x *' (x + ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (x *' (x + ((t *' t) *' t02s2)))))) / ((denominator (x *' (x + ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' r))) is Element of RAT+
((x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r)) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)) is Element of RAT+
numerator ((x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator ((x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator ((x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator ((x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r))))) / ((denominator ((x *' (x + ((t *' t) *' t02s2))) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is Element of RAT+
x *' x is Element of RAT+
(numerator x) *^ (numerator x) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator x) *^ (denominator x) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator x) *^ (numerator x)) / ((denominator x) *^ (denominator x)) is Element of RAT+
(x *' x) + (((t *' t) *' t02s2) *' x) is Element of RAT+
numerator (x *' x) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (x *' x)) *^ (denominator (((t *' t) *' t02s2) *' x)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (x *' x) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t *' t) *' t02s2) *' x)) *^ (denominator (x *' x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (x *' x)) *^ (denominator (((t *' t) *' t02s2) *' x))) +^ ((numerator (((t *' t) *' t02s2) *' x)) *^ (denominator (x *' x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (x *' x)) *^ (denominator (((t *' t) *' t02s2) *' x)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (x *' x)) *^ (denominator (((t *' t) *' t02s2) *' x))) +^ ((numerator (((t *' t) *' t02s2) *' x)) *^ (denominator (x *' x)))) / ((denominator (x *' x)) *^ (denominator (((t *' t) *' t02s2) *' x))) is Element of RAT+
((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r) is Element of RAT+
numerator ((x *' x) + (((t *' t) *' t02s2) *' x)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((x *' x) + (((t *' t) *' t02s2) *' x))) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((x *' x) + (((t *' t) *' t02s2) *' x)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t *' t) *' t02s2) *' r)) *^ (denominator ((x *' x) + (((t *' t) *' t02s2) *' x))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((x *' x) + (((t *' t) *' t02s2) *' x))) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator ((x *' x) + (((t *' t) *' t02s2) *' x)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((x *' x) + (((t *' t) *' t02s2) *' x))) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((x *' x) + (((t *' t) *' t02s2) *' x))) *^ (denominator (((t *' t) *' t02s2) *' r))) +^ ((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator ((x *' x) + (((t *' t) *' t02s2) *' x))))) / ((denominator ((x *' x) + (((t *' t) *' t02s2) *' x))) *^ (denominator (((t *' t) *' t02s2) *' r))) is Element of RAT+
(((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r)) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)) is Element of RAT+
numerator (((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator (((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator (((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator (((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r))))) / ((denominator (((x *' x) + (((t *' t) *' t02s2) *' x)) + (((t *' t) *' t02s2) *' r))) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is Element of RAT+
(((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)) is Element of RAT+
(numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator (((t *' t) *' t02s2) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator (((t *' t) *' t02s2) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ (denominator (((t *' t) *' t02s2) *' r)))) / ((denominator (((t *' t) *' t02s2) *' r)) *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is Element of RAT+
((x *' x) + (((t *' t) *' t02s2) *' x)) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is Element of RAT+
denominator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((x *' x) + (((t *' t) *' t02s2) *' x))) *^ (denominator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator ((x *' x) + (((t *' t) *' t02s2) *' x))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((x *' x) + (((t *' t) *' t02s2) *' x))) *^ (denominator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) +^ ((numerator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator ((x *' x) + (((t *' t) *' t02s2) *' x)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((x *' x) + (((t *' t) *' t02s2) *' x))) *^ (denominator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((x *' x) + (((t *' t) *' t02s2) *' x))) *^ (denominator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) +^ ((numerator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator ((x *' x) + (((t *' t) *' t02s2) *' x))))) / ((denominator ((x *' x) + (((t *' t) *' t02s2) *' x))) *^ (denominator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) is Element of RAT+
(((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is Element of RAT+
(numerator (((t *' t) *' t02s2) *' x)) *^ (denominator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((t *' t) *' t02s2) *' x)) *^ (denominator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) +^ ((numerator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((t *' t) *' t02s2) *' x)) *^ (denominator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((t *' t) *' t02s2) *' x)) *^ (denominator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) +^ ((numerator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) *^ (denominator (((t *' t) *' t02s2) *' x)))) / ((denominator (((t *' t) *' t02s2) *' x)) *^ (denominator ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) is Element of RAT+
(x *' x) + ((((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is Element of RAT+
denominator ((((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (x *' x)) *^ (denominator ((((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator ((((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) *^ (denominator (x *' x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (x *' x)) *^ (denominator ((((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))))) +^ ((numerator ((((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) *^ (denominator (x *' x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (x *' x)) *^ (denominator ((((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (x *' x)) *^ (denominator ((((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))))) +^ ((numerator ((((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))))) *^ (denominator (x *' x)))) / ((denominator (x *' x)) *^ (denominator ((((t *' t) *' t02s2) *' x) + ((((t *' t) *' t02s2) *' r) + (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))))) is Element of RAT+
(x *' x) + (t *' t) is Element of RAT+
(numerator (x *' x)) *^ (denominator (t *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (t *' t)) *^ (denominator (x *' x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (x *' x)) *^ (denominator (t *' t))) +^ ((numerator (t *' t)) *^ (denominator (x *' x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (x *' x)) *^ (denominator (t *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (x *' x)) *^ (denominator (t *' t))) +^ ((numerator (t *' t)) *^ (denominator (x *' x)))) / ((denominator (x *' x)) *^ (denominator (t *' t))) is Element of RAT+
two + (t *' t) is Element of RAT+
(numerator two) *^ (denominator (t *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (t *' t)) *^ (denominator two) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (denominator (t *' t))) +^ ((numerator (t *' t)) *^ (denominator two)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator two) *^ (denominator (t *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator two) *^ (denominator (t *' t))) +^ ((numerator (t *' t)) *^ (denominator two))) / ((denominator two) *^ (denominator (t *' t))) is Element of RAT+
t0x is Element of RAT+
t0x *' t0x is Element of RAT+
numerator t0x is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator t0x) *^ (numerator t0x) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator t0x is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator t0x) *^ (denominator t0x) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator t0x) *^ (numerator t0x)) / ((denominator t0x) *^ (denominator t0x)) is Element of RAT+
half *' two is Element of RAT+
(numerator half) *^ (numerator two) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator half) *^ (denominator two) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator half) *^ (numerator two)) / ((denominator half) *^ (denominator two)) is Element of RAT+
one *' one is Element of RAT+
(numerator one) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator one) *^ (numerator one)) / ((denominator one) *^ (denominator one)) is Element of RAT+
two *' r is Element of RAT+
(numerator two) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator two) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (numerator r)) / ((denominator two) *^ (denominator r)) is Element of RAT+
one *' r is Element of RAT+
(numerator one) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator one) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator one) *^ (numerator r)) / ((denominator one) *^ (denominator r)) is Element of RAT+
r *' one is Element of RAT+
(numerator r) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator one)) / ((denominator r) *^ (denominator one)) is Element of RAT+
half *' half is Element of RAT+
(numerator half) *^ (numerator half) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator half) *^ (denominator half) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator half) *^ (numerator half)) / ((denominator half) *^ (denominator half)) is Element of RAT+
t02s2 is Element of RAT+
(half *' half) + t02s2 is Element of RAT+
numerator (half *' half) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator t02s2 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (half *' half)) *^ (denominator t02s2) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator t02s2 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator (half *' half) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator t02s2) *^ (denominator (half *' half)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (half *' half)) *^ (denominator t02s2)) +^ ((numerator t02s2) *^ (denominator (half *' half))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (half *' half)) *^ (denominator t02s2) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (half *' half)) *^ (denominator t02s2)) +^ ((numerator t02s2) *^ (denominator (half *' half)))) / ((denominator (half *' half)) *^ (denominator t02s2)) is Element of RAT+
(r *' r) + t02s2 is Element of RAT+
(numerator (r *' r)) *^ (denominator t02s2) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator t02s2) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' r)) *^ (denominator t02s2)) +^ ((numerator t02s2) *^ (denominator (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' r)) *^ (denominator t02s2) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' r)) *^ (denominator t02s2)) +^ ((numerator t02s2) *^ (denominator (r *' r)))) / ((denominator (r *' r)) *^ (denominator t02s2)) is Element of RAT+
half *' one is Element of RAT+
(numerator half) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator half) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator half) *^ (numerator one)) / ((denominator half) *^ (denominator one)) is Element of RAT+
2t9 is Element of RAT+
(two *' r) *' 2t9 is Element of RAT+
numerator (two *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
numerator 2t9 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (two *' r)) *^ (numerator 2t9) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (two *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator 2t9 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator (two *' r)) *^ (denominator 2t9) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (two *' r)) *^ (numerator 2t9)) / ((denominator (two *' r)) *^ (denominator 2t9)) is Element of RAT+
(half *' half) *' 2t9 is Element of RAT+
(numerator (half *' half)) *^ (numerator 2t9) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (half *' half)) *^ (denominator 2t9) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (half *' half)) *^ (numerator 2t9)) / ((denominator (half *' half)) *^ (denominator 2t9)) is Element of RAT+
t0x is Element of RAT+
((half *' half) *' 2t9) + t0x is Element of RAT+
numerator ((half *' half) *' 2t9) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator t0x is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((half *' half) *' 2t9)) *^ (denominator t0x) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator t0x is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator ((half *' half) *' 2t9) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator t0x) *^ (denominator ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((half *' half) *' 2t9)) *^ (denominator t0x)) +^ ((numerator t0x) *^ (denominator ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((half *' half) *' 2t9)) *^ (denominator t0x) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((half *' half) *' 2t9)) *^ (denominator t0x)) +^ ((numerator t0x) *^ (denominator ((half *' half) *' 2t9)))) / ((denominator ((half *' half) *' 2t9)) *^ (denominator t0x)) is Element of RAT+
r + t0x is Element of RAT+
(numerator r) *^ (denominator t0x) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator t0x) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (denominator t0x)) +^ ((numerator t0x) *^ (denominator r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator t0x) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator r) *^ (denominator t0x)) +^ ((numerator t0x) *^ (denominator r))) / ((denominator r) *^ (denominator t0x)) is Element of RAT+
((half *' half) *' 2t9) *' (two *' r) is Element of RAT+
(numerator ((half *' half) *' 2t9)) *^ (numerator (two *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((half *' half) *' 2t9)) *^ (denominator (two *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((half *' half) *' 2t9)) *^ (numerator (two *' r))) / ((denominator ((half *' half) *' 2t9)) *^ (denominator (two *' r))) is Element of RAT+
(half *' half) *' one is Element of RAT+
(numerator (half *' half)) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (half *' half)) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (half *' half)) *^ (numerator one)) / ((denominator (half *' half)) *^ (denominator one)) is Element of RAT+
((half *' half) *' 2t9) *' t0x is Element of RAT+
(numerator ((half *' half) *' 2t9)) *^ (numerator t0x) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((half *' half) *' 2t9)) *^ (numerator t0x)) / ((denominator ((half *' half) *' 2t9)) *^ (denominator t0x)) is Element of RAT+
((half *' half) *' 2t9) *' r is Element of RAT+
(numerator ((half *' half) *' 2t9)) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((half *' half) *' 2t9)) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((half *' half) *' 2t9)) *^ (numerator r)) / ((denominator ((half *' half) *' 2t9)) *^ (denominator r)) is Element of RAT+
(((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r) is Element of RAT+
numerator (((half *' half) *' 2t9) *' t0x) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator (((half *' half) *' 2t9) *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator (((half *' half) *' 2t9) *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator (((half *' half) *' 2t9) *' t0x) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' t0x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' t0x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' t0x)))) / ((denominator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' r))) is Element of RAT+
((half *' half) *' 2t9) *' ((half *' half) *' 2t9) is Element of RAT+
(numerator ((half *' half) *' 2t9)) *^ (numerator ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((half *' half) *' 2t9)) *^ (denominator ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((half *' half) *' 2t9)) *^ (numerator ((half *' half) *' 2t9))) / ((denominator ((half *' half) *' 2t9)) *^ (denominator ((half *' half) *' 2t9))) is Element of RAT+
((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r)) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) is Element of RAT+
numerator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r))))) / ((denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is Element of RAT+
(((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) is Element of RAT+
(numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (((half *' half) *' 2t9) *' t0x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (((half *' half) *' 2t9) *' t0x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (((half *' half) *' 2t9) *' t0x)))) / ((denominator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is Element of RAT+
((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r) is Element of RAT+
numerator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((half *' half) *' 2t9) *' r)) *^ (denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))))) / ((denominator ((((half *' half) *' 2t9) *' t0x) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' r))) is Element of RAT+
(((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' r) is Element of RAT+
(numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' r)))) / ((denominator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' r))) is Element of RAT+
(((half *' half) *' 2t9) *' r) *' one is Element of RAT+
(numerator (((half *' half) *' 2t9) *' r)) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((half *' half) *' 2t9) *' r)) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((half *' half) *' 2t9) *' r)) *^ (numerator one)) / ((denominator (((half *' half) *' 2t9) *' r)) *^ (denominator one)) is Element of RAT+
((((half *' half) *' 2t9) *' r) *' one) + (((half *' half) *' 2t9) *' r) is Element of RAT+
numerator ((((half *' half) *' 2t9) *' r) *' one) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((((half *' half) *' 2t9) *' r) *' one) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((half *' half) *' 2t9) *' r)) *^ (denominator ((((half *' half) *' 2t9) *' r) *' one)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator ((((half *' half) *' 2t9) *' r) *' one))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator ((((half *' half) *' 2t9) *' r) *' one)))) / ((denominator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator (((half *' half) *' 2t9) *' r))) is Element of RAT+
((((half *' half) *' 2t9) *' r) *' one) + ((((half *' half) *' 2t9) *' r) *' one) is Element of RAT+
(numerator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator ((((half *' half) *' 2t9) *' r) *' one)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator ((((half *' half) *' 2t9) *' r) *' one))) +^ ((numerator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator ((((half *' half) *' 2t9) *' r) *' one))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator ((((half *' half) *' 2t9) *' r) *' one)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator ((((half *' half) *' 2t9) *' r) *' one))) +^ ((numerator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator ((((half *' half) *' 2t9) *' r) *' one)))) / ((denominator ((((half *' half) *' 2t9) *' r) *' one)) *^ (denominator ((((half *' half) *' 2t9) *' r) *' one))) is Element of RAT+
r *' ((half *' half) *' 2t9) is Element of RAT+
(numerator r) *^ (numerator ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator ((half *' half) *' 2t9))) / ((denominator r) *^ (denominator ((half *' half) *' 2t9))) is Element of RAT+
(r *' ((half *' half) *' 2t9)) *' two is Element of RAT+
numerator (r *' ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' ((half *' half) *' 2t9))) *^ (numerator two) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (r *' ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator (r *' ((half *' half) *' 2t9))) *^ (denominator two) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' ((half *' half) *' 2t9))) *^ (numerator two)) / ((denominator (r *' ((half *' half) *' 2t9))) *^ (denominator two)) is Element of RAT+
r *' two is Element of RAT+
(numerator r) *^ (numerator two) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator two) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator two)) / ((denominator r) *^ (denominator two)) is Element of RAT+
((half *' half) *' 2t9) *' (r *' two) is Element of RAT+
numerator (r *' two) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((half *' half) *' 2t9)) *^ (numerator (r *' two)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (r *' two) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator ((half *' half) *' 2t9)) *^ (denominator (r *' two)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((half *' half) *' 2t9)) *^ (numerator (r *' two))) / ((denominator ((half *' half) *' 2t9)) *^ (denominator (r *' two))) is Element of RAT+
t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) is Element of RAT+
(numerator t02s2) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator t02s2) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator t02s2) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator t02s2) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator t02s2) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator t02s2))) / ((denominator t02s2) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is Element of RAT+
(t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) + (half *' half) is Element of RAT+
numerator (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (half *' half)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (half *' half)) *^ (denominator (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (half *' half))) +^ ((numerator (half *' half)) *^ (denominator (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (half *' half)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (half *' half))) +^ ((numerator (half *' half)) *^ (denominator (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))))) / ((denominator (t02s2 + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (half *' half))) is Element of RAT+
(r *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) is Element of RAT+
(numerator (r *' r)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' r)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' r)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' r)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (r *' r)))) / ((denominator (r *' r)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is Element of RAT+
t0x + ((half *' half) *' 2t9) is Element of RAT+
((numerator t0x) *^ (denominator ((half *' half) *' 2t9))) +^ ((numerator ((half *' half) *' 2t9)) *^ (denominator t0x)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator t0x) *^ (denominator ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator t0x) *^ (denominator ((half *' half) *' 2t9))) +^ ((numerator ((half *' half) *' 2t9)) *^ (denominator t0x))) / ((denominator t0x) *^ (denominator ((half *' half) *' 2t9))) is Element of RAT+
t0x *' (t0x + ((half *' half) *' 2t9)) is Element of RAT+
numerator (t0x + ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator t0x) *^ (numerator (t0x + ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (t0x + ((half *' half) *' 2t9)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator t0x) *^ (denominator (t0x + ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator t0x) *^ (numerator (t0x + ((half *' half) *' 2t9)))) / ((denominator t0x) *^ (denominator (t0x + ((half *' half) *' 2t9)))) is Element of RAT+
(t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r) is Element of RAT+
numerator (t0x *' (t0x + ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (t0x *' (t0x + ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (t0x *' (t0x + ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (t0x *' (t0x + ((half *' half) *' 2t9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (t0x *' (t0x + ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (t0x *' (t0x + ((half *' half) *' 2t9))))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (t0x *' (t0x + ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (t0x *' (t0x + ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (t0x *' (t0x + ((half *' half) *' 2t9)))))) / ((denominator (t0x *' (t0x + ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' r))) is Element of RAT+
((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r)) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) is Element of RAT+
numerator ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r))))) / ((denominator ((t0x *' (t0x + ((half *' half) *' 2t9))) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is Element of RAT+
t0x *' t0x is Element of RAT+
(numerator t0x) *^ (numerator t0x) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator t0x) *^ (denominator t0x) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator t0x) *^ (numerator t0x)) / ((denominator t0x) *^ (denominator t0x)) is Element of RAT+
(t0x *' t0x) + (((half *' half) *' 2t9) *' t0x) is Element of RAT+
numerator (t0x *' t0x) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (t0x *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' t0x)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (t0x *' t0x) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (t0x *' t0x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (t0x *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' t0x))) +^ ((numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (t0x *' t0x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (t0x *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' t0x)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (t0x *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' t0x))) +^ ((numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator (t0x *' t0x)))) / ((denominator (t0x *' t0x)) *^ (denominator (((half *' half) *' 2t9) *' t0x))) is Element of RAT+
((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r) is Element of RAT+
numerator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((half *' half) *' 2t9) *' r)) *^ (denominator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) *^ (denominator (((half *' half) *' 2t9) *' r))) +^ ((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))))) / ((denominator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) *^ (denominator (((half *' half) *' 2t9) *' r))) is Element of RAT+
(((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r)) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) is Element of RAT+
numerator (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r))))) / ((denominator (((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + (((half *' half) *' 2t9) *' r))) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is Element of RAT+
(((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)) is Element of RAT+
(numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (((half *' half) *' 2t9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (((half *' half) *' 2t9) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) +^ ((numerator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) *^ (denominator (((half *' half) *' 2t9) *' r)))) / ((denominator (((half *' half) *' 2t9) *' r)) *^ (denominator (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is Element of RAT+
((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is Element of RAT+
denominator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) *^ (denominator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) *^ (denominator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) +^ ((numerator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) *^ (denominator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) *^ (denominator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) +^ ((numerator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))))) / ((denominator ((t0x *' t0x) + (((half *' half) *' 2t9) *' t0x))) *^ (denominator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) is Element of RAT+
(((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))) is Element of RAT+
(numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' t0x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) +^ ((numerator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' t0x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((half *' half) *' 2t9) *' t0x)) *^ (denominator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (((half *' half) *' 2t9) *' t0x)) *^ (denominator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) +^ ((numerator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) *^ (denominator (((half *' half) *' 2t9) *' t0x)))) / ((denominator (((half *' half) *' 2t9) *' t0x)) *^ (denominator ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) is Element of RAT+
(t0x *' t0x) + ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is Element of RAT+
denominator ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (t0x *' t0x)) *^ (denominator ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) *^ (denominator (t0x *' t0x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (t0x *' t0x)) *^ (denominator ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))))) +^ ((numerator ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) *^ (denominator (t0x *' t0x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (t0x *' t0x)) *^ (denominator ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (t0x *' t0x)) *^ (denominator ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))))) +^ ((numerator ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9))))) *^ (denominator (t0x *' t0x)))) / ((denominator (t0x *' t0x)) *^ (denominator ((((half *' half) *' 2t9) *' t0x) + ((((half *' half) *' 2t9) *' r) + (((half *' half) *' 2t9) *' ((half *' half) *' 2t9)))))) is Element of RAT+
(t0x *' t0x) + (half *' half) is Element of RAT+
(numerator (t0x *' t0x)) *^ (denominator (half *' half)) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (half *' half)) *^ (denominator (t0x *' t0x)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (t0x *' t0x)) *^ (denominator (half *' half))) +^ ((numerator (half *' half)) *^ (denominator (t0x *' t0x))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (t0x *' t0x)) *^ (denominator (half *' half)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (t0x *' t0x)) *^ (denominator (half *' half))) +^ ((numerator (half *' half)) *^ (denominator (t0x *' t0x)))) / ((denominator (t0x *' t0x)) *^ (denominator (half *' half))) is Element of RAT+
two + (half *' half) is Element of RAT+
(numerator two) *^ (denominator (half *' half)) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (half *' half)) *^ (denominator two) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (denominator (half *' half))) +^ ((numerator (half *' half)) *^ (denominator two)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator two) *^ (denominator (half *' half)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator two) *^ (denominator (half *' half))) +^ ((numerator (half *' half)) *^ (denominator two))) / ((denominator two) *^ (denominator (half *' half))) is Element of RAT+
c₁₈ is Element of RAT+
c₁₈ *' c₁₈ is Element of RAT+
numerator c₁₈ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator c₁₈) *^ (numerator c₁₈) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator c₁₈ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator c₁₈) *^ (denominator c₁₈) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator c₁₈) *^ (numerator c₁₈)) / ((denominator c₁₈) *^ (denominator c₁₈)) is Element of RAT+
two / 1 is Element of RAT+
two *^ ((denominator r) *^ (denominator r)) is epsilon-transitive epsilon-connected ordinal natural finite set
1 *^ ((numerator r) *^ (numerator r)) is epsilon-transitive epsilon-connected ordinal natural finite set
eps is epsilon-transitive epsilon-connected ordinal natural finite set
2 *^ eps is epsilon-transitive epsilon-connected ordinal natural finite set
eps *^ (2 *^ eps) is epsilon-transitive epsilon-connected ordinal natural finite set
2 *^ (eps *^ (2 *^ eps)) is epsilon-transitive epsilon-connected ordinal natural finite set
eps *^ eps is epsilon-transitive epsilon-connected ordinal natural finite set
2 *^ (eps *^ eps) is epsilon-transitive epsilon-connected ordinal natural finite set
t is epsilon-transitive epsilon-connected ordinal natural finite set
2 *^ t is epsilon-transitive epsilon-connected ordinal natural finite set
d2 is Element of RAT+
r is Element of RAT+
3r9 is Element of RAT+
3r9 is Element of RAT+
r + r is Element of RAT+
numerator r is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator r is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator r) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (denominator r)) +^ ((numerator r) *^ (denominator r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator r) *^ (denominator r)) +^ ((numerator r) *^ (denominator r))) / ((denominator r) *^ (denominator r)) is Element of RAT+
(r + r) + r is Element of RAT+
numerator (r + r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r + r)) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (r + r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator r) *^ (denominator (r + r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r + r)) *^ (denominator r)) +^ ((numerator r) *^ (denominator (r + r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r + r)) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r + r)) *^ (denominator r)) +^ ((numerator r) *^ (denominator (r + r)))) / ((denominator (r + r)) *^ (denominator r)) is Element of RAT+
3r9 is Element of RAT+
((r + r) + r) *' 3r9 is Element of RAT+
numerator ((r + r) + r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
numerator 3r9 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((r + r) + r)) *^ (numerator 3r9) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((r + r) + r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator 3r9 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator ((r + r) + r)) *^ (denominator 3r9) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((r + r) + r)) *^ (numerator 3r9)) / ((denominator ((r + r) + r)) *^ (denominator 3r9)) is Element of RAT+
r *' r is Element of RAT+
(numerator r) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator r)) / ((denominator r) *^ (denominator r)) is Element of RAT+
rr is Element of RAT+
(r *' r) + rr is Element of RAT+
numerator (r *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator rr is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' r)) *^ (denominator rr) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator rr is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator (r *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator rr) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' r)) *^ (denominator rr)) +^ ((numerator rr) *^ (denominator (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' r)) *^ (denominator rr) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' r)) *^ (denominator rr)) +^ ((numerator rr) *^ (denominator (r *' r)))) / ((denominator (r *' r)) *^ (denominator rr)) is Element of RAT+
two + rr is Element of RAT+
(numerator two) *^ (denominator rr) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator rr) *^ (denominator two) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (denominator rr)) +^ ((numerator rr) *^ (denominator two)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator two) *^ (denominator rr) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator two) *^ (denominator rr)) +^ ((numerator rr) *^ (denominator two))) / ((denominator two) *^ (denominator rr)) is Element of RAT+
rr *' 3r9 is Element of RAT+
(numerator rr) *^ (numerator 3r9) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator rr) *^ (denominator 3r9) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator rr) *^ (numerator 3r9)) / ((denominator rr) *^ (denominator 3r9)) is Element of RAT+
t is Element of RAT+
t *' t is Element of RAT+
numerator t is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator t) *^ (numerator t) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator t is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator t) *^ (denominator t) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator t) *^ (numerator t)) / ((denominator t) *^ (denominator t)) is Element of RAT+
r *' (rr *' 3r9) is Element of RAT+
numerator (rr *' 3r9) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator r) *^ (numerator (rr *' 3r9)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (rr *' 3r9) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator r) *^ (denominator (rr *' 3r9)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator (rr *' 3r9))) / ((denominator r) *^ (denominator (rr *' 3r9))) is Element of RAT+
(rr *' 3r9) *' (rr *' 3r9) is Element of RAT+
(numerator (rr *' 3r9)) *^ (numerator (rr *' 3r9)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (rr *' 3r9)) *^ (denominator (rr *' 3r9)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (rr *' 3r9)) *^ (numerator (rr *' 3r9))) / ((denominator (rr *' 3r9)) *^ (denominator (rr *' 3r9))) is Element of RAT+
(rr *' 3r9) *' r is Element of RAT+
(numerator (rr *' 3r9)) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (rr *' 3r9)) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (rr *' 3r9)) *^ (numerator r)) / ((denominator (rr *' 3r9)) *^ (denominator r)) is Element of RAT+
(r *' (rr *' 3r9)) + ((rr *' 3r9) *' r) is Element of RAT+
numerator (r *' (rr *' 3r9)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator ((rr *' 3r9) *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' (rr *' 3r9))) *^ (denominator ((rr *' 3r9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator ((rr *' 3r9) *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator (r *' (rr *' 3r9)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((rr *' 3r9) *' r)) *^ (denominator (r *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' (rr *' 3r9))) *^ (denominator ((rr *' 3r9) *' r))) +^ ((numerator ((rr *' 3r9) *' r)) *^ (denominator (r *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' (rr *' 3r9))) *^ (denominator ((rr *' 3r9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' (rr *' 3r9))) *^ (denominator ((rr *' 3r9) *' r))) +^ ((numerator ((rr *' 3r9) *' r)) *^ (denominator (r *' (rr *' 3r9))))) / ((denominator (r *' (rr *' 3r9))) *^ (denominator ((rr *' 3r9) *' r))) is Element of RAT+
((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + (r *' (rr *' 3r9)) is Element of RAT+
numerator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) *^ (denominator (r *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' (rr *' 3r9))) *^ (denominator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) *^ (denominator (r *' (rr *' 3r9)))) +^ ((numerator (r *' (rr *' 3r9))) *^ (denominator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) *^ (denominator (r *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) *^ (denominator (r *' (rr *' 3r9)))) +^ ((numerator (r *' (rr *' 3r9))) *^ (denominator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))))) / ((denominator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) *^ (denominator (r *' (rr *' 3r9)))) is Element of RAT+
((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9)) is Element of RAT+
denominator ((rr *' 3r9) *' (rr *' 3r9)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) *^ (denominator ((rr *' 3r9) *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator ((rr *' 3r9) *' (rr *' 3r9)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((rr *' 3r9) *' (rr *' 3r9))) *^ (denominator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) *^ (denominator ((rr *' 3r9) *' (rr *' 3r9)))) +^ ((numerator ((rr *' 3r9) *' (rr *' 3r9))) *^ (denominator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) *^ (denominator ((rr *' 3r9) *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) *^ (denominator ((rr *' 3r9) *' (rr *' 3r9)))) +^ ((numerator ((rr *' 3r9) *' (rr *' 3r9))) *^ (denominator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))))) / ((denominator ((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r))) *^ (denominator ((rr *' 3r9) *' (rr *' 3r9)))) is Element of RAT+
r + (rr *' 3r9) is Element of RAT+
(numerator r) *^ (denominator (rr *' 3r9)) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (rr *' 3r9)) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (denominator (rr *' 3r9))) +^ ((numerator (rr *' 3r9)) *^ (denominator r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator r) *^ (denominator (rr *' 3r9))) +^ ((numerator (rr *' 3r9)) *^ (denominator r))) / ((denominator r) *^ (denominator (rr *' 3r9))) is Element of RAT+
t is Element of RAT+
t *' t is Element of RAT+
numerator t is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator t) *^ (numerator t) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator t is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator t) *^ (denominator t) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator t) *^ (numerator t)) / ((denominator t) *^ (denominator t)) is Element of RAT+
r *' t is Element of RAT+
(numerator r) *^ (numerator t) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator t) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator t)) / ((denominator r) *^ (denominator t)) is Element of RAT+
(rr *' 3r9) *' t is Element of RAT+
(numerator (rr *' 3r9)) *^ (numerator t) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (rr *' 3r9)) *^ (denominator t) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (rr *' 3r9)) *^ (numerator t)) / ((denominator (rr *' 3r9)) *^ (denominator t)) is Element of RAT+
(r *' t) + ((rr *' 3r9) *' t) is Element of RAT+
numerator (r *' t) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator ((rr *' 3r9) *' t) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' t)) *^ (denominator ((rr *' 3r9) *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator ((rr *' 3r9) *' t) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
denominator (r *' t) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((rr *' 3r9) *' t)) *^ (denominator (r *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' t)) *^ (denominator ((rr *' 3r9) *' t))) +^ ((numerator ((rr *' 3r9) *' t)) *^ (denominator (r *' t))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' t)) *^ (denominator ((rr *' 3r9) *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' t)) *^ (denominator ((rr *' 3r9) *' t))) +^ ((numerator ((rr *' 3r9) *' t)) *^ (denominator (r *' t)))) / ((denominator (r *' t)) *^ (denominator ((rr *' 3r9) *' t))) is Element of RAT+
(r *' r) + (r *' (rr *' 3r9)) is Element of RAT+
(numerator (r *' r)) *^ (denominator (r *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (r *' (rr *' 3r9))) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' r)) *^ (denominator (r *' (rr *' 3r9)))) +^ ((numerator (r *' (rr *' 3r9))) *^ (denominator (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' r)) *^ (denominator (r *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' r)) *^ (denominator (r *' (rr *' 3r9)))) +^ ((numerator (r *' (rr *' 3r9))) *^ (denominator (r *' r)))) / ((denominator (r *' r)) *^ (denominator (r *' (rr *' 3r9)))) is Element of RAT+
((r *' r) + (r *' (rr *' 3r9))) + ((rr *' 3r9) *' t) is Element of RAT+
numerator ((r *' r) + (r *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((r *' r) + (r *' (rr *' 3r9)))) *^ (denominator ((rr *' 3r9) *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((r *' r) + (r *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((rr *' 3r9) *' t)) *^ (denominator ((r *' r) + (r *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((r *' r) + (r *' (rr *' 3r9)))) *^ (denominator ((rr *' 3r9) *' t))) +^ ((numerator ((rr *' 3r9) *' t)) *^ (denominator ((r *' r) + (r *' (rr *' 3r9))))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((r *' r) + (r *' (rr *' 3r9)))) *^ (denominator ((rr *' 3r9) *' t)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((r *' r) + (r *' (rr *' 3r9)))) *^ (denominator ((rr *' 3r9) *' t))) +^ ((numerator ((rr *' 3r9) *' t)) *^ (denominator ((r *' r) + (r *' (rr *' 3r9)))))) / ((denominator ((r *' r) + (r *' (rr *' 3r9)))) *^ (denominator ((rr *' 3r9) *' t))) is Element of RAT+
((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)) is Element of RAT+
(numerator ((rr *' 3r9) *' r)) *^ (denominator ((rr *' 3r9) *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator ((rr *' 3r9) *' (rr *' 3r9))) *^ (denominator ((rr *' 3r9) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((rr *' 3r9) *' r)) *^ (denominator ((rr *' 3r9) *' (rr *' 3r9)))) +^ ((numerator ((rr *' 3r9) *' (rr *' 3r9))) *^ (denominator ((rr *' 3r9) *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((rr *' 3r9) *' r)) *^ (denominator ((rr *' 3r9) *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((rr *' 3r9) *' r)) *^ (denominator ((rr *' 3r9) *' (rr *' 3r9)))) +^ ((numerator ((rr *' 3r9) *' (rr *' 3r9))) *^ (denominator ((rr *' 3r9) *' r)))) / ((denominator ((rr *' 3r9) *' r)) *^ (denominator ((rr *' 3r9) *' (rr *' 3r9)))) is Element of RAT+
((r *' r) + (r *' (rr *' 3r9))) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))) is Element of RAT+
denominator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((r *' r) + (r *' (rr *' 3r9)))) *^ (denominator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) *^ (denominator ((r *' r) + (r *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((r *' r) + (r *' (rr *' 3r9)))) *^ (denominator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))))) +^ ((numerator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) *^ (denominator ((r *' r) + (r *' (rr *' 3r9))))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((r *' r) + (r *' (rr *' 3r9)))) *^ (denominator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((r *' r) + (r *' (rr *' 3r9)))) *^ (denominator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))))) +^ ((numerator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) *^ (denominator ((r *' r) + (r *' (rr *' 3r9)))))) / ((denominator ((r *' r) + (r *' (rr *' 3r9)))) *^ (denominator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))))) is Element of RAT+
(r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))) is Element of RAT+
(numerator (r *' (rr *' 3r9))) *^ (denominator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) *^ (denominator (r *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' (rr *' 3r9))) *^ (denominator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))))) +^ ((numerator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) *^ (denominator (r *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' (rr *' 3r9))) *^ (denominator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' (rr *' 3r9))) *^ (denominator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))))) +^ ((numerator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) *^ (denominator (r *' (rr *' 3r9))))) / ((denominator (r *' (rr *' 3r9))) *^ (denominator (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))))) is Element of RAT+
(r *' r) + ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) is Element of RAT+
denominator ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' r)) *^ (denominator ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))))) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' r)) *^ (denominator ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))))) +^ ((numerator ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))))) *^ (denominator (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' r)) *^ (denominator ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' r)) *^ (denominator ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))))) +^ ((numerator ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9))))) *^ (denominator (r *' r)))) / ((denominator (r *' r)) *^ (denominator ((r *' (rr *' 3r9)) + (((rr *' 3r9) *' r) + ((rr *' 3r9) *' (rr *' 3r9)))))) is Element of RAT+
(r *' r) + (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9))) is Element of RAT+
denominator (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' r)) *^ (denominator (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9)))) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' r)) *^ (denominator (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9))))) +^ ((numerator (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9)))) *^ (denominator (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' r)) *^ (denominator (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' r)) *^ (denominator (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9))))) +^ ((numerator (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9)))) *^ (denominator (r *' r)))) / ((denominator (r *' r)) *^ (denominator (((r *' (rr *' 3r9)) + ((rr *' 3r9) *' r)) + ((rr *' 3r9) *' (rr *' 3r9))))) is Element of RAT+
(rr *' 3r9) *' (r + r) is Element of RAT+
(numerator (rr *' 3r9)) *^ (numerator (r + r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (rr *' 3r9)) *^ (denominator (r + r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (rr *' 3r9)) *^ (numerator (r + r))) / ((denominator (rr *' 3r9)) *^ (denominator (r + r))) is Element of RAT+
((rr *' 3r9) *' (r + r)) + (r *' (rr *' 3r9)) is Element of RAT+
numerator ((rr *' 3r9) *' (r + r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((rr *' 3r9) *' (r + r))) *^ (denominator (r *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((rr *' 3r9) *' (r + r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' (rr *' 3r9))) *^ (denominator ((rr *' 3r9) *' (r + r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((rr *' 3r9) *' (r + r))) *^ (denominator (r *' (rr *' 3r9)))) +^ ((numerator (r *' (rr *' 3r9))) *^ (denominator ((rr *' 3r9) *' (r + r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((rr *' 3r9) *' (r + r))) *^ (denominator (r *' (rr *' 3r9))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((rr *' 3r9) *' (r + r))) *^ (denominator (r *' (rr *' 3r9)))) +^ ((numerator (r *' (rr *' 3r9))) *^ (denominator ((rr *' 3r9) *' (r + r))))) / ((denominator ((rr *' 3r9) *' (r + r))) *^ (denominator (r *' (rr *' 3r9)))) is Element of RAT+
(rr *' 3r9) *' ((r + r) + r) is Element of RAT+
(numerator (rr *' 3r9)) *^ (numerator ((r + r) + r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (rr *' 3r9)) *^ (denominator ((r + r) + r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (rr *' 3r9)) *^ (numerator ((r + r) + r))) / ((denominator (rr *' 3r9)) *^ (denominator ((r + r) + r))) is Element of RAT+
rr *' one is Element of RAT+
(numerator rr) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator rr) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator rr) *^ (numerator one)) / ((denominator rr) *^ (denominator one)) is Element of RAT+
s is Element of RAT+
s *' s is Element of RAT+
numerator s is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator s) *^ (numerator s) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator s is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator s) *^ (denominator s) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator s) *^ (numerator s)) / ((denominator s) *^ (denominator s)) is Element of RAT+
r + d2 is Element of RAT+
denominator d2 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator r) *^ (denominator d2) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator d2 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator d2) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (denominator d2)) +^ ((numerator d2) *^ (denominator r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator d2) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator r) *^ (denominator d2)) +^ ((numerator d2) *^ (denominator r))) / ((denominator r) *^ (denominator d2)) is Element of RAT+
(rr *' 3r9) *' ((r + r) + r) is Element of RAT+
numerator (rr *' 3r9) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (rr *' 3r9)) *^ (numerator ((r + r) + r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (rr *' 3r9) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator (rr *' 3r9)) *^ (denominator ((r + r) + r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (rr *' 3r9)) *^ (numerator ((r + r) + r))) / ((denominator (rr *' 3r9)) *^ (denominator ((r + r) + r))) is Element of RAT+
rr *' one is Element of RAT+
(numerator rr) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator rr) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator rr) *^ (numerator one)) / ((denominator rr) *^ (denominator one)) is Element of RAT+
r *' ((r + r) + r) is Element of RAT+
(numerator r) *^ (numerator ((r + r) + r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator ((r + r) + r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator ((r + r) + r))) / ((denominator r) *^ (denominator ((r + r) + r))) is Element of RAT+
a9 + half is Element of RAT+
(numerator a9) *^ (denominator half) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator half) *^ (denominator a9) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator a9) *^ (denominator half)) +^ ((numerator half) *^ (denominator a9)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator a9) *^ (denominator half) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator a9) *^ (denominator half)) +^ ((numerator half) *^ (denominator a9))) / ((denominator a9) *^ (denominator half)) is Element of RAT+
(a9 + half) *' r is Element of RAT+
numerator (a9 + half) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (a9 + half)) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (a9 + half) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator (a9 + half)) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (a9 + half)) *^ (numerator r)) / ((denominator (a9 + half)) *^ (denominator r)) is Element of RAT+
two *' one is Element of RAT+
(numerator two) *^ (numerator one) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator two) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (numerator one)) / ((denominator two) *^ (denominator one)) is Element of RAT+
one + half is Element of RAT+
(numerator one) *^ (denominator half) is epsilon-transitive epsilon-connected ordinal natural finite set
(numerator half) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator one) *^ (denominator half)) +^ ((numerator half) *^ (denominator one)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator one) *^ (denominator half) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator one) *^ (denominator half)) +^ ((numerator half) *^ (denominator one))) / ((denominator one) *^ (denominator half)) is Element of RAT+
two *' r is Element of RAT+
(numerator two) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator two) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (numerator r)) / ((denominator two) *^ (denominator r)) is Element of RAT+
t is Element of RAT+
(two *' r) *' (two *' r) is Element of RAT+
numerator (two *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (two *' r)) *^ (numerator (two *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (two *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator (two *' r)) *^ (denominator (two *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (two *' r)) *^ (numerator (two *' r))) / ((denominator (two *' r)) *^ (denominator (two *' r))) is Element of RAT+
(two *' r) *' t is Element of RAT+
numerator t is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (two *' r)) *^ (numerator t) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator t is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator (two *' r)) *^ (denominator t) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (two *' r)) *^ (numerator t)) / ((denominator (two *' r)) *^ (denominator t)) is Element of RAT+
t *' t is Element of RAT+
(numerator t) *^ (numerator t) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator t) *^ (denominator t) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator t) *^ (numerator t)) / ((denominator t) *^ (denominator t)) is Element of RAT+
(r *' ((r + r) + r)) + (r *' r) is Element of RAT+
numerator (r *' ((r + r) + r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' ((r + r) + r))) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (r *' ((r + r) + r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' r)) *^ (denominator (r *' ((r + r) + r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' ((r + r) + r))) *^ (denominator (r *' r))) +^ ((numerator (r *' r)) *^ (denominator (r *' ((r + r) + r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' ((r + r) + r))) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' ((r + r) + r))) *^ (denominator (r *' r))) +^ ((numerator (r *' r)) *^ (denominator (r *' ((r + r) + r))))) / ((denominator (r *' ((r + r) + r))) *^ (denominator (r *' r))) is Element of RAT+
r *' (r + r) is Element of RAT+
(numerator r) *^ (numerator (r + r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator (r + r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator (r + r))) / ((denominator r) *^ (denominator (r + r))) is Element of RAT+
(r *' (r + r)) + (r *' r) is Element of RAT+
numerator (r *' (r + r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' (r + r))) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (r *' (r + r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' r)) *^ (denominator (r *' (r + r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' (r + r))) *^ (denominator (r *' r))) +^ ((numerator (r *' r)) *^ (denominator (r *' (r + r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' (r + r))) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' (r + r))) *^ (denominator (r *' r))) +^ ((numerator (r *' r)) *^ (denominator (r *' (r + r))))) / ((denominator (r *' (r + r))) *^ (denominator (r *' r))) is Element of RAT+
((r *' (r + r)) + (r *' r)) + (r *' r) is Element of RAT+
numerator ((r *' (r + r)) + (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((r *' (r + r)) + (r *' r))) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((r *' (r + r)) + (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' r)) *^ (denominator ((r *' (r + r)) + (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((r *' (r + r)) + (r *' r))) *^ (denominator (r *' r))) +^ ((numerator (r *' r)) *^ (denominator ((r *' (r + r)) + (r *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((r *' (r + r)) + (r *' r))) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((r *' (r + r)) + (r *' r))) *^ (denominator (r *' r))) +^ ((numerator (r *' r)) *^ (denominator ((r *' (r + r)) + (r *' r))))) / ((denominator ((r *' (r + r)) + (r *' r))) *^ (denominator (r *' r))) is Element of RAT+
(r *' r) + (r *' r) is Element of RAT+
(numerator (r *' r)) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' r)) *^ (denominator (r *' r))) +^ ((numerator (r *' r)) *^ (denominator (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' r)) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' r)) *^ (denominator (r *' r))) +^ ((numerator (r *' r)) *^ (denominator (r *' r)))) / ((denominator (r *' r)) *^ (denominator (r *' r))) is Element of RAT+
(r *' (r + r)) + ((r *' r) + (r *' r)) is Element of RAT+
denominator ((r *' r) + (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' (r + r))) *^ (denominator ((r *' r) + (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator ((r *' r) + (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((r *' r) + (r *' r))) *^ (denominator (r *' (r + r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' (r + r))) *^ (denominator ((r *' r) + (r *' r)))) +^ ((numerator ((r *' r) + (r *' r))) *^ (denominator (r *' (r + r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' (r + r))) *^ (denominator ((r *' r) + (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' (r + r))) *^ (denominator ((r *' r) + (r *' r)))) +^ ((numerator ((r *' r) + (r *' r))) *^ (denominator (r *' (r + r))))) / ((denominator (r *' (r + r))) *^ (denominator ((r *' r) + (r *' r)))) is Element of RAT+
r *' (two *' r) is Element of RAT+
(numerator r) *^ (numerator (two *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator r) *^ (denominator (two *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator (two *' r))) / ((denominator r) *^ (denominator (two *' r))) is Element of RAT+
(r *' (two *' r)) + ((r *' r) + (r *' r)) is Element of RAT+
numerator (r *' (two *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' (two *' r))) *^ (denominator ((r *' r) + (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator (r *' (two *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator ((r *' r) + (r *' r))) *^ (denominator (r *' (two *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' (two *' r))) *^ (denominator ((r *' r) + (r *' r)))) +^ ((numerator ((r *' r) + (r *' r))) *^ (denominator (r *' (two *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' (two *' r))) *^ (denominator ((r *' r) + (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' (two *' r))) *^ (denominator ((r *' r) + (r *' r)))) +^ ((numerator ((r *' r) + (r *' r))) *^ (denominator (r *' (two *' r))))) / ((denominator (r *' (two *' r))) *^ (denominator ((r *' r) + (r *' r)))) is Element of RAT+
two *' (r *' r) is Element of RAT+
(numerator two) *^ (numerator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator two) *^ (denominator (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (numerator (r *' r))) / ((denominator two) *^ (denominator (r *' r))) is Element of RAT+
(r *' (two *' r)) + (two *' (r *' r)) is Element of RAT+
denominator (two *' (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (r *' (two *' r))) *^ (denominator (two *' (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator (two *' (r *' r)) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator (two *' (r *' r))) *^ (denominator (r *' (two *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (r *' (two *' r))) *^ (denominator (two *' (r *' r)))) +^ ((numerator (two *' (r *' r))) *^ (denominator (r *' (two *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (r *' (two *' r))) *^ (denominator (two *' (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (r *' (two *' r))) *^ (denominator (two *' (r *' r)))) +^ ((numerator (two *' (r *' r))) *^ (denominator (r *' (two *' r))))) / ((denominator (r *' (two *' r))) *^ (denominator (two *' (r *' r)))) is Element of RAT+
(two *' (r *' r)) + (two *' (r *' r)) is Element of RAT+
(numerator (two *' (r *' r))) *^ (denominator (two *' (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (two *' (r *' r))) *^ (denominator (two *' (r *' r)))) +^ ((numerator (two *' (r *' r))) *^ (denominator (two *' (r *' r)))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (two *' (r *' r))) *^ (denominator (two *' (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator (two *' (r *' r))) *^ (denominator (two *' (r *' r)))) +^ ((numerator (two *' (r *' r))) *^ (denominator (two *' (r *' r))))) / ((denominator (two *' (r *' r))) *^ (denominator (two *' (r *' r)))) is Element of RAT+
two *' (two *' (r *' r)) is Element of RAT+
(numerator two) *^ (numerator (two *' (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator two) *^ (denominator (two *' (r *' r))) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (numerator (two *' (r *' r)))) / ((denominator two) *^ (denominator (two *' (r *' r)))) is Element of RAT+
(two *' r) *' r is Element of RAT+
(numerator (two *' r)) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (two *' r)) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (two *' r)) *^ (numerator r)) / ((denominator (two *' r)) *^ (denominator r)) is Element of RAT+
two *' ((two *' r) *' r) is Element of RAT+
numerator ((two *' r) *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator two) *^ (numerator ((two *' r) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator ((two *' r) *' r) is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator two) *^ (denominator ((two *' r) *' r)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator two) *^ (numerator ((two *' r) *' r))) / ((denominator two) *^ (denominator ((two *' r) *' r))) is Element of RAT+
s is Element of RAT+
s *' s is Element of RAT+
numerator s is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator s) *^ (numerator s) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator s is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator s) *^ (denominator s) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator s) *^ (numerator s)) / ((denominator s) *^ (denominator s)) is Element of RAT+
one + d2 is Element of RAT+
denominator d2 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator one) *^ (denominator d2) is epsilon-transitive epsilon-connected ordinal natural finite set
numerator d2 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator d2) *^ (denominator one) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator one) *^ (denominator d2)) +^ ((numerator d2) *^ (denominator one)) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator one) *^ (denominator d2) is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator one) *^ (denominator d2)) +^ ((numerator d2) *^ (denominator one))) / ((denominator one) *^ (denominator d2)) is Element of RAT+
one *' r is Element of RAT+
(numerator one) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator one) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator one) *^ (numerator r)) / ((denominator one) *^ (denominator r)) is Element of RAT+
t is Element of RAT+
a9 *' half is Element of RAT+
(numerator a9) *^ (numerator half) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator a9) *^ (denominator half) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator a9) *^ (numerator half)) / ((denominator a9) *^ (denominator half)) is Element of RAT+
{ [b₁,one] where b₁ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : verum } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,one] where b₁ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : verum } is Element of bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) }
r is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
3r9 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
[r,3r9] is V15() set
{r,3r9} is non empty set
{r} is non empty set
{{r,3r9},{r}} is non empty set
r is Element of RAT+
r *' r is Element of RAT+
numerator r is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator r) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator r is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator r) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator r)) / ((denominator r) *^ (denominator r)) is Element of RAT+
{ [b₁,one] where b₁ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : verum } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,one] where b₁ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : verum } is Element of bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) }
[:{()},RAT+:] is Relation-like set
r is set
3r9 is set
[r,3r9] is V15() set
{r,3r9} is non empty set
{r} is non empty set
{{r,3r9},{r}} is non empty set
[:{()},RAT+:] is Relation-like set
r is Element of RAT+
r *' r is Element of RAT+
numerator r is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(numerator r) *^ (numerator r) is epsilon-transitive epsilon-connected ordinal natural finite set
denominator r is epsilon-transitive epsilon-connected ordinal natural finite Element of omega
(denominator r) *^ (denominator r) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator r) *^ (numerator r)) / ((denominator r) *^ (denominator r)) is Element of RAT+
[:{()},REAL+:] is Relation-like set
REAL+ \/ [:{()},REAL+:] is non empty set
[:{()},():] is Relation-like non finite set
[:{()},RAT+:] is Relation-like set
() \/ [:{()},():] is non empty set
RAT+ \/ [:{()},RAT+:] is non empty set
c is epsilon-transitive epsilon-connected ordinal set
d1 is epsilon-transitive epsilon-connected ordinal set
c *^ d1 is epsilon-transitive epsilon-connected ordinal set
d2 is epsilon-transitive epsilon-connected ordinal set
c *^ d2 is epsilon-transitive epsilon-connected ordinal set
[1,2] is V15() set
{1,2} is non empty set
{{1,2},{1}} is non empty set
[:{()},():] is Relation-like non finite set
() \/ [:{()},():] is non empty set
[(),1] is V15() set
{{(),1},{()}} is non empty set
[:{()},():] is Relation-like non finite set
() \/ [:{()},():] is non empty set
[(),()] is V15() set
{(),()} is non empty set
{{(),()},{()}} is non empty set
{[(),()]} is Relation-like non empty set
[(),()] is V15() set
{(),()} is non empty set
{{(),()},{()}} is non empty set
{(),[(),()]} is non empty set
() \/ {(),[(),()]} is non empty set
() is set