:: NUMBERS semantic presentation

RAT+ is non empty set

{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } is set

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

bool () is set
DEDEKIND_CUTS is non empty Element of bool ()
REAL+ is non empty set
{ b1 where b1 is Element of bool RAT+ : for b2 being Element of RAT+ holds
( not b2 in b1 or ( ( for b3 being Element of RAT+ holds
( not b3 <=' b2 or b3 in b1 ) ) & ex b3 being Element of RAT+ st
( b3 in b1 & not b3 <=' b2 ) ) )
}
is set

is non empty set
{ b1 where b1 is Element of bool RAT+ : for b2 being Element of RAT+ holds
( not b2 in b1 or ( ( for b3 being Element of RAT+ holds
( not b3 <=' b2 or b3 in b1 ) ) & ex b3 being Element of RAT+ st
( b3 in b1 & not b3 <=' b2 ) ) )
}
\ is Element of bool { b1 where b1 is Element of bool RAT+ : for b2 being Element of RAT+ holds
( not b2 in b1 or ( ( for b3 being Element of RAT+ holds
( not b3 <=' b2 or b3 in b1 ) ) & ex b3 being Element of RAT+ st
( b3 in b1 & not b3 <=' b2 ) ) )
}

bool { b1 where b1 is Element of bool RAT+ : for b2 being Element of RAT+ holds
( not b2 in b1 or ( ( for b3 being Element of RAT+ holds
( not b3 <=' b2 or b3 in b1 ) ) & ex b3 being Element of RAT+ st
( b3 in b1 & not b3 <=' b2 ) ) )
}
is set

RAT+ \/ DEDEKIND_CUTS is non empty set

{ { b2 where b2 is Element of RAT+ : not b1 <=' b2 } where b1 is Element of RAT+ : not b1 = {} } is set
\ { { b2 where b2 is Element of RAT+ : not b1 <=' b2 } where b1 is Element of RAT+ : not b1 = {} } is Element of bool

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

is non empty set

REAL+ \/ is non empty set
is V15() set
is non empty set
is non empty set

() \ is Element of bool ()
bool () is set
() is set
{{},1} is non empty set
Funcs ({{},1},()) is functional non empty FUNCTION_DOMAIN of {{},1},()
{ b1 where b1 is Relation-like Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},()) : b1 . 1 = {} } is set
(Funcs ({{},1},())) \ { b1 where b1 is Relation-like Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},()) : b1 . 1 = {} } is Element of bool (Funcs ({{},1},()))
bool (Funcs ({{},1},())) is set
((Funcs ({{},1},())) \ { b1 where b1 is Relation-like Function-like V14({{},1}) quasi_total Element of Funcs ({{},1},()) : b1 . 1 = {} } ) \/ () is non empty set

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

omega \/ is non empty set
() \ is Element of bool ()
bool () 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() quasi_total Element of bool [:,():]
is non empty set

bool [:,():] 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
is non empty set
{{one,two},} is non empty set
{[{},a9],[one,two]} is Relation-like non empty set
is non empty 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
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite Element of () : ( b1,b2 are_relative_prime & not b2 = {} ) } 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
{{d2}} is non empty set
{ [b1,one] where b1 is epsilon-transitive epsilon-connected ordinal natural finite Element of () : verum } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite Element of () : ( b1,b2 are_relative_prime & not b2 = {} ) } \ { [b1,one] where b1 is epsilon-transitive epsilon-connected ordinal natural finite Element of () : verum } is Element of bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite Element of () : ( b1,b2 are_relative_prime & not b2 = {} ) }
bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite Element of () : ( b1,b2 are_relative_prime & not b2 = {} ) } 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},} 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+

{(),one} is non empty set
Funcs ({(),one},()) is functional non empty FUNCTION_DOMAIN of {(),one},()
{ b1 where b1 is Relation-like Function-like V14({(),one}) quasi_total Element of Funcs ({(),one},()) : b1 . 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 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},())) \ { b1 where b1 is Relation-like Function-like V14({(),one}) quasi_total Element of Funcs ({(),one},()) : b1 . one = () } is Element of bool (Funcs ({(),one},()))
bool (Funcs ({(),one},())) is set

{()} is non empty set

RAT+ \/ [:{()},RAT+:] is non empty set
REAL+ \/ [:{()},REAL+:] is non empty set

c is Element of REAL+
d1 is Element of REAL+
d2 is Element of RAT+
DD is Element of RAT+

d1 is Element of RAT+
a9 + d1 is Element of RAT+

(() *^ ()) +^ (() *^ ()) is epsilon-transitive epsilon-connected ordinal natural finite set

((() *^ ()) +^ (() *^ ())) / (() *^ ()) is Element of RAT+

{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 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
(((a9 div^ 2) *^ 2) *^ (((a9 div^ 2) *^ 2) +^ 1)) +^ ((one *^ ((a9 div^ 2) *^ 2)) +^ ()) 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

(() +^ ()) / () is Element of RAT+

c is Element of RAT+
c + c is Element of RAT+

(() *^ ()) +^ (() *^ ()) is epsilon-transitive epsilon-connected ordinal natural finite set

((() *^ ()) +^ (() *^ ())) / (() *^ ()) is Element of RAT+
two *' c is Element of RAT+

((numerator two) *^ ()) / ((denominator two) *^ ()) is Element of RAT+
one *' c is Element of RAT+

(() *^ ()) / ( *^ ()) is Element of RAT+
() + c is Element of RAT+

((numerator ()) *^ ()) +^ (() *^ (denominator ())) is epsilon-transitive epsilon-connected ordinal natural finite set

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

((numerator ()) *^ (denominator ())) +^ ((numerator ()) *^ (denominator ())) is epsilon-transitive epsilon-connected ordinal natural finite set

(((numerator ()) *^ (denominator ())) +^ ((numerator ()) *^ (denominator ()))) / ((denominator ()) *^ (denominator ())) is Element of RAT+
{ b1 where b1 is Element of RAT+ : S1[b1] } is set

two *' two is Element of RAT+

((numerator two) *^ (numerator two)) / ((denominator two) *^ (denominator two)) is Element of RAT+

1 \/ {1} is non empty set
a9 is Element of RAT+
a9 *' a9 is Element of RAT+

(() *^ ()) / (() *^ ()) 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+

(() *^ ()) / (() *^ ()) is Element of RAT+
DD *' d2 is Element of RAT+

(() *^ ()) / (() *^ ()) is Element of RAT+
d2 *' d2 is Element of RAT+

(() *^ ()) / (() *^ ()) is Element of RAT+
half is Element of RAT+
half *' half is Element of RAT+

((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 two) *^ (numerator half)) / ((denominator two) *^ (denominator half)) is Element of RAT+
{ { b2 where b2 is Element of RAT+ : not b1 <=' b2 } where b1 is Element of RAT+ : not b1 = () } is set
r is Element of RAT+
{ b1 where b1 is Element of RAT+ : not r <=' b1 } is set

r *' r is Element of RAT+

(() *^ ()) / (() *^ ()) is Element of RAT+
eps is Element of RAT+
eps is Element of RAT+
two + eps is Element of RAT+

((numerator two) *^ (denominator eps)) +^ ((numerator eps) *^ (denominator two)) 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)) *^ (denominator eps)) +^ ((numerator eps) *^ (denominator (r *' r))) 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+

(() *^ ()) / (() *^ ) is Element of RAT+
t *' t is Element of RAT+

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

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

(() *^ ()) / ( *^ ()) is Element of RAT+

() / () is Element of RAT+
two *' r is Element of RAT+

((numerator two) *^ ()) / ((denominator two) *^ ()) is Element of RAT+
s is Element of RAT+
(t *' t) + s is Element of RAT+

((numerator (t *' t)) *^ ()) +^ (() *^ (denominator (t *' t))) is epsilon-transitive epsilon-connected ordinal natural finite set

(((numerator (t *' t)) *^ ()) +^ (() *^ (denominator (t *' t)))) / ((denominator (t *' t)) *^ ()) is Element of RAT+
(r *' r) + s 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)))) / ((denominator (r *' r)) *^ ()) is Element of RAT+
t02s2 is Element of RAT+
(two *' r) *' t02s2 is Element of RAT+

(numerator (two *' r)) *^ (numerator t02s2) is epsilon-transitive epsilon-connected ordinal natural finite set

(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)) / ((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 set

() *^ (denominator ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t *' t) *' t02s2)) *^ ()) +^ (() *^ (denominator ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((t *' t) *' t02s2)) *^ () is epsilon-transitive epsilon-connected ordinal natural finite set
(((numerator ((t *' t) *' t02s2)) *^ ()) +^ (() *^ (denominator ((t *' t) *' t02s2)))) / ((denominator ((t *' t) *' t02s2)) *^ ()) is Element of RAT+
r + x is Element of RAT+

(() *^ ()) +^ (() *^ ()) is epsilon-transitive epsilon-connected ordinal natural finite set

((() *^ ()) +^ (() *^ ())) / (() *^ ()) 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)) *^ ()) / ((denominator (t *' t)) *^ ) is Element of RAT+
((t *' t) *' t02s2) *' x is Element of RAT+
(numerator ((t *' t) *' t02s2)) *^ () is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t *' t) *' t02s2)) *^ ()) / ((denominator ((t *' t) *' t02s2)) *^ ()) is Element of RAT+
((t *' t) *' t02s2) *' r is Element of RAT+
(numerator ((t *' t) *' t02s2)) *^ () is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator ((t *' t) *' t02s2)) *^ () is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator ((t *' t) *' t02s2)) *^ ()) / ((denominator ((t *' t) *' t02s2)) *^ ()) 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)) *^ () is epsilon-transitive epsilon-connected ordinal natural finite set
(denominator (((t *' t) *' t02s2) *' r)) *^ is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (((t *' t) *' t02s2) *' r)) *^ ()) / ((denominator (((t *' t) *' t02s2) *' r)) *^ ) 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 ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite set
() *^ (denominator ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite set
(() *^ (numerator ((t *' t) *' t02s2))) / (() *^ (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 two)) / (() *^ (denominator two)) is Element of RAT+
((t *' t) *' t02s2) *' (r *' two) is Element of RAT+

(numerator ((t *' t) *' t02s2)) *^ (numerator (r *' two)) is epsilon-transitive epsilon-connected ordinal natural finite set

(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+
() *^ (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 set
(() *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ ()) is epsilon-transitive epsilon-connected ordinal natural finite set
() *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
((() *^ (denominator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2)))) +^ ((numerator (((t *' t) *' t02s2) *' ((t *' t) *' t02s2))) *^ ())) / (() *^ (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+
(() *^ (denominator ((t *' t) *' t02s2))) +^ ((numerator ((t *' t) *' t02s2)) *^ ()) is epsilon-transitive epsilon-connected ordinal natural finite set
() *^ (denominator ((t *' t) *' t02s2)) is epsilon-transitive epsilon-connected ordinal natural finite set
((() *^ (denominator ((t *' t) *' t02s2))) +^ ((numerator ((t *' t) *' t02s2)) *^ ())) / (() *^ (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))) *^ () 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))) *^ () is epsilon-transitive epsilon-connected ordinal natural finite set
((numerator (x + ((t *' t) *' t02s2))) *^ ()) / ((denominator (x + ((t *' t) *' t02s2))) *^ ()) 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 + ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
() *^ (denominator (x + ((t *' t) *' t02s2))) is epsilon-transitive epsilon-connected ordinal natural finite set
(() *^ (numerator (x + ((t *' t) *' t02s2)))) / (() *^ (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+

(() *^ ()) / (() *^ ()) is Element of RAT+
(x *' x) + (((t *' t) *' t02s2) *' x) is Element of RAT+

(numerator (x *' x)) *^ (denominator (((t *' t) *' t02s2) *' x)) is epsilon-transitive epsilon-connected ordinal natural finite set

(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)