:: ARYTM_2 semantic presentation

omega is non empty epsilon-transitive epsilon-connected ordinal set

RAT+ is non empty set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

{ [b

1 is non empty epsilon-transitive epsilon-connected ordinal natural Element of omega

{ [b

{ [b

bool { [b

( { [b

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Element of RAT+

one is non empty epsilon-transitive epsilon-connected ordinal natural Element of RAT+

bool RAT+ is non empty set

{ b

( not b

( not b

( b

{RAT+} is non empty set

{ b

( not b

( not b

( b

( not b

( not b

( b

bool { b

( not b

( not b

( b

bool (bool RAT+) is non empty set

RA is set

rone is Element of bool RAT+

() is Element of bool (bool RAT+)

{ b

RA is set

rone is Element of RAT+

RA is Element of RAT+

RA is non empty Element of bool RAT+

rone is Element of RAT+

x is Element of RAT+

y is Element of RAT+

x is Element of RAT+

x is Element of RAT+

RAT+ \/ () is non empty set

{ { b

(RAT+ \/ ()) \ { { b

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

() is set

rone is set

x is set

[rone,x] is set

{rone,x} is non empty set

{rone} is non empty set

{{rone,x},{rone}} is non empty set

y is Element of bool RAT+

y9 is Element of RAT+

A is Element of RAT+

y9 is Element of RAT+

A is Element of RAT+

B is Element of RAT+

rone is set

x is Element of RAT+

{ b

y is set

y9 is Element of RAT+

y is non empty Element of bool RAT+

y9 is Element of RAT+

A is Element of RAT+

A is Element of RAT+

RAT+ \/ { b

( not b

( not b

( b

( { b

( not b

( not b

( b

( not b

( not b

( b

RAT+ \/ (( { b

( not b

( not b

( b

() \ { { b

{ [b

{ [b

bool { [b

( { [b

rone is Element of ()

x is Element of RAT+

{ b

y9 is set

A is Element of RAT+

y9 is Element of RAT+

y9 is Element of bool RAT+

A is Element of RAT+

B is Element of RAT+

B is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

A is Element of ()

y9 is Element of RAT+

x is Element of ()

{ b

A is Element of RAT+

y is Element of ()

{ b

B is Element of ()

x9 is Element of ()

rone is set

[{},rone] is set

{{},rone} is non empty set

{{}} is non empty set

{{{},rone},{{}}} is non empty set

rone is Element of RAT+

x is Element of RAT+

rone is Element of ()

x is Element of ()

y is Element of ()

y9 is Element of RAT+

A is Element of RAT+

B is Element of RAT+

x is Element of RAT+

y is Element of ()

y9 is Element of ()

A is Element of RAT+

B is Element of RAT+

x9 is Element of RAT+

x is Element of RAT+

{ b

y is Element of RAT+

y9 is Element of RAT+

x is Element of ()

rone is Element of RAT+

x is set

y is Element of bool RAT+

rone is Element of bool RAT+

x is Element of RAT+

y is Element of RAT+

() /\ RAT+ is Element of bool (bool RAT+)

{{}} is non empty set

rone is set

x is non empty Element of bool RAT+

y is Element of RAT+

rone is Element of ()

(rone) is Element of ()

{ b

x is set

y is Element of RAT+

x is Element of RAT+

{ b

x is Element of RAT+

{ b

rone is Element of ()

(rone) is Element of ()

x is Element of RAT+

y is Element of RAT+

y is Element of RAT+

x is Element of RAT+

x is Element of RAT+

y is Element of RAT+

x is Element of RAT+

rone is Element of ()

(rone) is Element of ()

((rone)) is Element of ()

x is Element of RAT+

x is Element of RAT+

y is Element of RAT+

{ b

y9 is set

A is Element of RAT+

y9 is set

A is Element of RAT+

RAT+ /\ () is Element of bool (bool RAT+)

x is Element of RAT+

rone is set

x is set

y is set

A is Element of bool RAT+

A is set

x9 is Element of bool RAT+

B is Element of RAT+

y9 is Element of RAT+

x9 is Element of bool RAT+

x9 is Element of bool RAT+

rone is Element of ()

x is Element of ()

y is Element of RAT+

y9 is Element of RAT+

A is Element of RAT+

B is Element of RAT+

y is Element of ()

y9 is Element of ()

A is Element of RAT+

B is Element of RAT+

rone is Element of RAT+

x is Element of RAT+

y is Element of ()

y9 is Element of ()

A is Element of RAT+

B is Element of RAT+

rone is set

x is Element of bool RAT+

y is non empty Element of bool RAT+

y9 is Element of RAT+

A is Element of RAT+

B is Element of RAT+

x9 is Element of RAT+

B is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

rone is Element of RAT+

x is Element of RAT+

y is set

y9 is Element of bool RAT+

rone is set

x is non empty Element of bool RAT+

y is Element of RAT+

rone is Element of RAT+

x is set

{ b

y is set

y9 is Element of ()

A is Element of RAT+

y is set

y9 is Element of RAT+

rone is Element of ()

(rone) is Element of ()

rone is Element of ()

(rone) is Element of ()

x is Element of ()

(x) is Element of ()

y is Element of RAT+

{ b

y9 is Element of RAT+

{ b

A is Element of RAT+

y is Element of RAT+

{ b

y9 is Element of RAT+

y is Element of RAT+

{ b

y9 is Element of RAT+

A is Element of RAT+

rone is Element of ()

x is Element of ()

y is Element of RAT+

y9 is Element of RAT+

rone is Element of ()

(rone) is Element of ()

x is Element of ()

(x) is Element of ()

rone is Element of ()

(rone) is Element of ()

((rone)) is Element of ()

(((rone))) is Element of ()

rone is Element of ()

x is Element of ()

{ (b

y9 is set

A is Element of RAT+

B is Element of RAT+

A + B is Element of RAT+

numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator A),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator A),(denominator B)),K73((numerator B),(denominator A))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator A),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator A),(denominator B)),K73((numerator B),(denominator A))) / K73((denominator A),(denominator B)) is Element of RAT+

A is Element of RAT+

y9 is Element of bool RAT+

B is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

x9 + r is Element of RAT+

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator r),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator r)),K73((numerator r),(denominator x9))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator r)),K73((numerator r),(denominator x9))) / K73((denominator x9),(denominator r)) is Element of RAT+

s is Element of RAT+

t1 is Element of RAT+

t2 is Element of RAT+

t1 + t2 is Element of RAT+

numerator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t1),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set

numerator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t2),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator t1),(denominator t2)),K73((numerator t2),(denominator t1))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator t1),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator t1),(denominator t2)),K73((numerator t2),(denominator t1))) / K73((denominator t1),(denominator t2)) is Element of RAT+

s is Element of RAT+

s + r is Element of RAT+

numerator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator s),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

denominator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator r),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator s),(denominator r)),K73((numerator r),(denominator s))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator s),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator s),(denominator r)),K73((numerator r),(denominator s))) / K73((denominator s),(denominator r)) is Element of RAT+

t1 is Element of RAT+

B is Element of RAT+

A + B is Element of RAT+

numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator A),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator A),(denominator B)),K73((numerator B),(denominator A))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator A),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator A),(denominator B)),K73((numerator B),(denominator A))) / K73((denominator A),(denominator B)) is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

x9 + r is Element of RAT+

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator r),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator r)),K73((numerator r),(denominator x9))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator r)),K73((numerator r),(denominator x9))) / K73((denominator x9),(denominator r)) is Element of RAT+

y is Element of ()

y9 is Element of ()

A is Element of ()

{ (b

{ (b

r is set

s is Element of RAT+

t1 is Element of RAT+

s + t1 is Element of RAT+

numerator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator s),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

numerator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t1),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator s),(denominator t1)),K73((numerator t1),(denominator s))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator s),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator s),(denominator t1)),K73((numerator t1),(denominator s))) / K73((denominator s),(denominator t1)) is Element of RAT+

r is set

s is Element of RAT+

t1 is Element of RAT+

s + t1 is Element of RAT+

numerator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator s),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

numerator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t1),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator s),(denominator t1)),K73((numerator t1),(denominator s))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator s),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator s),(denominator t1)),K73((numerator t1),(denominator s))) / K73((denominator s),(denominator t1)) is Element of RAT+

rone is set

x is Element of bool RAT+

rone is Element of ()

x is Element of ()

{ (b

y is set

y9 is Element of RAT+

A is Element of RAT+

y9 *' A is Element of RAT+

numerator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator y9),(numerator A)) is epsilon-transitive epsilon-connected ordinal natural set

denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator y9),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator y9),(numerator A)) / K73((denominator y9),(denominator A)) is Element of RAT+

y9 is set

A is Element of RAT+

B is Element of RAT+

A *' B is Element of RAT+

numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator A),(numerator B)) is epsilon-transitive epsilon-connected ordinal natural set

denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator A),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator A),(numerator B)) / K73((denominator A),(denominator B)) is Element of RAT+

y9 is Element of bool RAT+

A is Element of RAT+

B is Element of RAT+

x9 is Element of RAT+

B *' x9 is Element of RAT+

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(numerator x9)) is epsilon-transitive epsilon-connected ordinal natural set

denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator B),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator B),(numerator x9)) / K73((denominator B),(denominator x9)) is Element of RAT+

r is Element of RAT+

s is Element of RAT+

B *' s is Element of RAT+

numerator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(numerator s)) is epsilon-transitive epsilon-connected ordinal natural set

denominator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator B),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator B),(numerator s)) / K73((denominator B),(denominator s)) is Element of RAT+

r is Element of RAT+

s is Element of RAT+

s *' r is Element of RAT+

numerator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator s),(numerator r)) is epsilon-transitive epsilon-connected ordinal natural set

denominator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator s),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator s),(numerator r)) / K73((denominator s),(denominator r)) is Element of RAT+

B *' r is Element of RAT+

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(numerator r)) is epsilon-transitive epsilon-connected ordinal natural set

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator B),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator B),(numerator r)) / K73((denominator B),(denominator r)) is Element of RAT+

A is Element of RAT+

B is Element of RAT+

A *' B is Element of RAT+

numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator A),(numerator B)) is epsilon-transitive epsilon-connected ordinal natural set

denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator A),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator A),(numerator B)) / K73((denominator A),(denominator B)) is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

x9 *' r is Element of RAT+

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(numerator r)) is epsilon-transitive epsilon-connected ordinal natural set

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator x9),(numerator r)) / K73((denominator x9),(denominator r)) is Element of RAT+

y is Element of ()

y9 is Element of ()

A is Element of ()

{ (b

{ (b

B is set

x9 is Element of RAT+

r is Element of RAT+

x9 *' r is Element of RAT+

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(numerator r)) is epsilon-transitive epsilon-connected ordinal natural set

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator x9),(numerator r)) / K73((denominator x9),(denominator r)) is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

x9 *' r is Element of RAT+

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(numerator r)) is epsilon-transitive epsilon-connected ordinal natural set

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator x9),(numerator r)) / K73((denominator x9),(denominator r)) is Element of RAT+

s is Element of RAT+

t1 is Element of RAT+

s *' t1 is Element of RAT+

numerator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator s),(numerator t1)) is epsilon-transitive epsilon-connected ordinal natural set

denominator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator s),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator s),(numerator t1)) / K73((denominator s),(denominator t1)) is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

x9 *' r is Element of RAT+

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(numerator r)) is epsilon-transitive epsilon-connected ordinal natural set

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator x9),(numerator r)) / K73((denominator x9),(denominator r)) is Element of RAT+

x is Element of ()

rone is Element of ()

(rone) is Element of ()

(x) is Element of ()

((rone),(x)) is Element of ()

{ (b

(((rone),(x))) is Element of ()

y is Element of ()

A is Element of ()

y is Element of ()

y9 is Element of ()

(y9) is Element of ()

(A) is Element of ()

((y9),(A)) is Element of ()

{ (b

(((y9),(A))) is Element of ()

((A),(y9)) is Element of ()

{ (b

(((A),(y9))) is Element of ()

((rone),(x)) is Element of ()

{ (b

(((rone),(x))) is Element of ()

y is Element of ()

y9 is Element of ()

(y9) is Element of ()

A is Element of ()

(A) is Element of ()

((y9),(A)) is Element of ()

{ (b

(((y9),(A))) is Element of ()

((A),(y9)) is Element of ()

{ (b

(((A),(y9))) is Element of ()

rone is Element of ()

x is Element of ()

(rone,x) is Element of ()

(rone) is Element of ()

(x) is Element of ()

((rone),(x)) is Element of ()

{ (b

(((rone),(x))) is Element of ()

A is set

B is Element of RAT+

x9 is Element of RAT+

B *' x9 is Element of RAT+

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(numerator x9)) is epsilon-transitive epsilon-connected ordinal natural set

denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator B),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator B),(numerator x9)) / K73((denominator B),(denominator x9)) is Element of RAT+

rone is Element of ()

x is Element of ()

(rone,x) is Element of ()

(x) is Element of ()

y is Element of RAT+

(rone) is Element of ()

y9 is Element of RAT+

y9 + y is Element of RAT+

numerator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator y is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator y9),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set

numerator y is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator y),(denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator y9),(denominator y)),K73((numerator y),(denominator y9))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator y9),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator y9),(denominator y)),K73((numerator y),(denominator y9))) / K73((denominator y9),(denominator y)) is Element of RAT+

{ (b

((rone),(x)) is Element of ()

(((rone),(x))) is Element of ()

rone is Element of ()

x is Element of ()

y is Element of ()

(x,y) is Element of ()

{ (b

(rone,(x,y)) is Element of ()

{ (b

(rone,x) is Element of ()

{ (b

((rone,x),y) is Element of ()

{ (b

y9 is set

A is Element of RAT+

B is Element of RAT+

A + B is Element of RAT+

numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator A),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator A),(denominator B)),K73((numerator B),(denominator A))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator A),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator A),(denominator B)),K73((numerator B),(denominator A))) / K73((denominator A),(denominator B)) is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

x9 + r is Element of RAT+

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator r),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator r)),K73((numerator r),(denominator x9))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator r)),K73((numerator r),(denominator x9))) / K73((denominator x9),(denominator r)) is Element of RAT+

A + x9 is Element of RAT+

K73((numerator A),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator x9),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator A),(denominator x9)),K73((numerator x9),(denominator A))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator A),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator A),(denominator x9)),K73((numerator x9),(denominator A))) / K73((denominator A),(denominator x9)) is Element of RAT+

(A + x9) + r is Element of RAT+

numerator (A + x9) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator (A + x9)),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

denominator (A + x9) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator r),(denominator (A + x9))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (A + x9)),(denominator r)),K73((numerator r),(denominator (A + x9)))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator (A + x9)),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (A + x9)),(denominator r)),K73((numerator r),(denominator (A + x9)))) / K73((denominator (A + x9)),(denominator r)) is Element of RAT+

rone is Element of ()

x is Element of ()

y is Element of ()

(x,y) is Element of ()

{ (b

(rone,(x,y)) is Element of ()

{ (b

(rone,x) is Element of ()

{ (b

((rone,x),y) is Element of ()

{ (b

rone is Element of ()

x is Element of ()

(rone,x) is Element of ()

{ (b

y is Element of RAT+

y9 is Element of RAT+

y + y9 is Element of RAT+

numerator y is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator y),(denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set

numerator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator y is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator y9),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator y),(denominator y9)),K73((numerator y9),(denominator y))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator y),(denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator y),(denominator y9)),K73((numerator y9),(denominator y))) / K73((denominator y),(denominator y9)) is Element of RAT+

rone is Element of ()

x is Element of ()

(rone,x) is Element of ()

y is Element of ()

(x,y) is Element of ()

(rone,(x,y)) is Element of ()

((rone,x),y) is Element of ()

(rone,y) is Element of ()

(x) is Element of ()

(y) is Element of ()

((x),(y)) is Element of ()

{ (b

(((x),(y))) is Element of ()

(rone) is Element of ()

((rone),(x)) is Element of ()

{ (b

(((rone),(x))) is Element of ()

(rone,(((x),(y)))) is Element of ()

((((x),(y)))) is Element of ()

((rone),((((x),(y))))) is Element of ()

{ (b

(((rone),((((x),(y)))))) is Element of ()

((rone),((x),(y))) is Element of ()

{ (b

(((rone),((x),(y)))) is Element of ()

(((rone),(x)),(y)) is Element of ()

{ (b

((((rone),(x)),(y))) is Element of ()

((((rone),(x)))) is Element of ()

(((((rone),(x)))),(y)) is Element of ()

{ (b

((((((rone),(x)))),(y))) is Element of ()

((((rone),(x))),y) is Element of ()

x is set

y is set

y9 is set

B is Element of bool RAT+

B is set

r is Element of bool RAT+

x9 is Element of RAT+

A is Element of RAT+

r is Element of bool RAT+

r is Element of bool RAT+

rone is set

rone is Element of RAT+

x is Element of RAT+

y is set

y9 is Element of bool RAT+

rone is Element of ()

x is Element of ()

y is Element of RAT+

y9 is Element of RAT+

A is Element of RAT+

B is Element of ()

y9 is Element of bool RAT+

y is Element of RAT+

A is Element of RAT+

B is Element of ()

y is Element of RAT+

y9 is Element of bool RAT+

A is Element of RAT+

{ b

x9 is set

r is Element of RAT+

x9 is set

r is Element of RAT+

B is Element of RAT+

B is Element of RAT+

x9 is Element of ()

y is Element of bool RAT+

y9 is Element of bool RAT+

A is Element of RAT+

B is Element of ()

rone is Element of ()

x is Element of ()

y is Element of ()

B is Element of RAT+

A is Element of RAT+

y9 is Element of RAT+

A is Element of RAT+

y9 is Element of RAT+

B is Element of bool RAT+

B is Element of bool RAT+

A is Element of RAT+

y9 is Element of RAT+

A is Element of bool RAT+

y9 is Element of RAT+

B is Element of bool RAT+

A is Element of RAT+

y9 is Element of RAT+

B is Element of bool RAT+

y9 is Element of bool RAT+

B is Element of bool RAT+

x9 is set

r is Element of RAT+

A is Element of RAT+

A is Element of bool RAT+

B is Element of bool RAT+

y9 is Element of RAT+

y9 is Element of bool RAT+

A is Element of bool RAT+

B is Element of bool RAT+

bool () is non empty set

x is Element of bool ()

rone is Element of bool ()

y is Element of ()

{ b

( b

A is Element of RAT+

A is Element of RAT+

B is Element of ()

x9 is Element of ()

r is Element of ()

s is Element of ()

t1 is Element of RAT+

s is Element of ()

t1 is Element of RAT+

t2 is Element of RAT+

xx is Element of ()

dr is Element of ()

dr is Element of ()

t2 is Element of ()

A is Element of RAT+

{ b

B is Element of RAT+

x9 is Element of RAT+

A is set

B is Element of RAT+

r is Element of ()

x9 is Element of ()

A is Element of RAT+

A is Element of RAT+

A is non empty Element of bool RAT+

B is Element of RAT+

x9 is Element of RAT+

s is Element of ()

r is Element of ()

B is Element of bool RAT+

x9 is Element of RAT+

r is Element of ()

s is Element of RAT+

t2 is Element of ()

t1 is Element of ()

s is Element of ()

B is Element of RAT+

x9 is Element of ()

r is Element of RAT+

t1 is Element of ()

s is Element of ()

r is Element of ()

s is Element of RAT+

t1 is Element of ()

s is Element of ()

t1 is Element of RAT+

B is Element of ()

x9 is Element of ()

r is Element of ()

s is Element of ()

t1 is Element of RAT+

s is Element of ()

t1 is Element of RAT+

t2 is Element of RAT+

xx is Element of ()

dr is Element of ()

t2 is Element of ()

A is Element of RAT+

rone is Element of ()

x is Element of ()

(rone,x) is Element of ()

{ (b

y is Element of RAT+

{} *' y is Element of RAT+

numerator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator y is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator {}),(numerator y)) is epsilon-transitive epsilon-connected ordinal natural set

denominator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator y is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator {}),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator {}),(numerator y)) / K73((denominator {}),(denominator y)) is Element of RAT+

y9 is Element of RAT+

y9 is Element of RAT+

A is Element of RAT+

A *' y is Element of RAT+

numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator A),(numerator y)) is epsilon-transitive epsilon-connected ordinal natural set

denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator A),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator A),(numerator y)) / K73((denominator A),(denominator y)) is Element of RAT+

B is Element of RAT+

B *' y is Element of RAT+

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(numerator y)) is epsilon-transitive epsilon-connected ordinal natural set

denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator B),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator B),(numerator y)) / K73((denominator B),(denominator y)) is Element of RAT+

B + one is Element of RAT+

denominator one is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(denominator one)) is epsilon-transitive epsilon-connected ordinal natural set

numerator one is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator one),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator B),(denominator one)),K73((numerator one),(denominator B))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator B),(denominator one)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator B),(denominator one)),K73((numerator one),(denominator B))) / K73((denominator B),(denominator one)) is Element of RAT+

(B + one) *' y is Element of RAT+

numerator (B + one) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator (B + one)),(numerator y)) is epsilon-transitive epsilon-connected ordinal natural set

denominator (B + one) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator (B + one)),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator (B + one)),(numerator y)) / K73((denominator (B + one)),(denominator y)) is Element of RAT+

one *' y is Element of RAT+

K73((numerator one),(numerator y)) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator one),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator one),(numerator y)) / K73((denominator one),(denominator y)) is Element of RAT+

(B *' y) + (one *' y) is Element of RAT+

numerator (B *' y) is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator (one *' y) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator (B *' y)),(denominator (one *' y))) is epsilon-transitive epsilon-connected ordinal natural set

numerator (one *' y) is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator (B *' y) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator (one *' y)),(denominator (B *' y))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (B *' y)),(denominator (one *' y))),K73((numerator (one *' y)),(denominator (B *' y)))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator (B *' y)),(denominator (one *' y))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (B *' y)),(denominator (one *' y))),K73((numerator (one *' y)),(denominator (B *' y)))) / K73((denominator (B *' y)),(denominator (one *' y))) is Element of RAT+

(B *' y) + y is Element of RAT+

K73((numerator (B *' y)),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator y),(denominator (B *' y))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (B *' y)),(denominator y)),K73((numerator y),(denominator (B *' y)))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator (B *' y)),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (B *' y)),(denominator y)),K73((numerator y),(denominator (B *' y)))) / K73((denominator (B *' y)),(denominator y)) is Element of RAT+

rone is Element of ()

x is Element of ()

(rone,x) is Element of ()

(rone) is Element of ()

(x) is Element of ()

((rone),(x)) is Element of ()

{ (b

(((rone),(x))) is Element of ()

((((rone),(x)))) is Element of ()

rone is Element of ()

x is Element of ()

y is Element of RAT+

{ b

( not b

A is set

B is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

x9 + B is Element of RAT+

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator B)),K73((numerator B),(denominator x9))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator x9),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator B)),K73((numerator B),(denominator x9))) / K73((denominator x9),(denominator B)) is Element of RAT+

y + {} is Element of RAT+

numerator y is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator y),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set

numerator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator y is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator {}),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator y),(denominator {})),K73((numerator {}),(denominator y))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator y),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator y),(denominator {})),K73((numerator {}),(denominator y))) / K73((denominator y),(denominator {})) is Element of RAT+

A is non empty Element of bool RAT+

B is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

s is Element of RAT+

r + x9 is Element of RAT+

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator r),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator r),(denominator x9)),K73((numerator x9),(denominator r))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator r),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator r),(denominator x9)),K73((numerator x9),(denominator r))) / K73((denominator r),(denominator x9)) is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

x9 + B is Element of RAT+

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator B)),K73((numerator B),(denominator x9))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator x9),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator B)),K73((numerator B),(denominator x9))) / K73((denominator x9),(denominator B)) is Element of RAT+

s is Element of RAT+

t1 is Element of RAT+

s + t1 is Element of RAT+

numerator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator s),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

numerator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator s is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t1),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator s),(denominator t1)),K73((numerator t1),(denominator s))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator s),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator s),(denominator t1)),K73((numerator t1),(denominator s))) / K73((denominator s),(denominator t1)) is Element of RAT+

t2 is Element of RAT+

t1 + t2 is Element of RAT+

denominator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t1),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set

numerator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t2),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator t1),(denominator t2)),K73((numerator t2),(denominator t1))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator t1),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator t1),(denominator t2)),K73((numerator t2),(denominator t1))) / K73((denominator t1),(denominator t2)) is Element of RAT+

x9 + s is Element of RAT+

K73((numerator x9),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator s),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator s)),K73((numerator s),(denominator x9))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator x9),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator s)),K73((numerator s),(denominator x9))) / K73((denominator x9),(denominator s)) is Element of RAT+

(x9 + s) + t1 is Element of RAT+

numerator (x9 + s) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator (x9 + s)),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

denominator (x9 + s) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t1),(denominator (x9 + s))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (x9 + s)),(denominator t1)),K73((numerator t1),(denominator (x9 + s)))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator (x9 + s)),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (x9 + s)),(denominator t1)),K73((numerator t1),(denominator (x9 + s)))) / K73((denominator (x9 + s)),(denominator t1)) is Element of RAT+

t2 + t1 is Element of RAT+

K72(K73((numerator t2),(denominator t1)),K73((numerator t1),(denominator t2))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator t2),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator t2),(denominator t1)),K73((numerator t1),(denominator t2))) / K73((denominator t2),(denominator t1)) is Element of RAT+

s is Element of RAT+

t1 is Element of RAT+

r + t1 is Element of RAT+

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator r),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

numerator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t1),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator r),(denominator t1)),K73((numerator t1),(denominator r))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator r),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator r),(denominator t1)),K73((numerator t1),(denominator r))) / K73((denominator r),(denominator t1)) is Element of RAT+

B + t1 is Element of RAT+

K73((numerator B),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator t1),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator B),(denominator t1)),K73((numerator t1),(denominator B))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator B),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator B),(denominator t1)),K73((numerator t1),(denominator B))) / K73((denominator B),(denominator t1)) is Element of RAT+

x9 + (B + t1) is Element of RAT+

denominator (B + t1) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(denominator (B + t1))) is epsilon-transitive epsilon-connected ordinal natural set

numerator (B + t1) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator (B + t1)),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator (B + t1))),K73((numerator (B + t1)),(denominator x9))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator x9),(denominator (B + t1))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator x9),(denominator (B + t1))),K73((numerator (B + t1)),(denominator x9))) / K73((denominator x9),(denominator (B + t1))) is Element of RAT+

B is Element of RAT+

x9 is Element of RAT+

r is Element of RAT+

s is Element of RAT+

r + x9 is Element of RAT+

numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator r),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator x9),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator r),(denominator x9)),K73((numerator x9),(denominator r))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator r),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator r),(denominator x9)),K73((numerator x9),(denominator r))) / K73((denominator r),(denominator x9)) is Element of RAT+

x9 is Element of ()

(rone,x9) is Element of ()

{ (b

s is set

t1 is Element of RAT+

t1 + {} is Element of RAT+

numerator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t1),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set

denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator {}),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator t1),(denominator {})),K73((numerator {}),(denominator t1))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator t1),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator t1),(denominator {})),K73((numerator {}),(denominator t1))) / K73((denominator t1),(denominator {})) is Element of RAT+

t1 is Element of RAT+

t2 is Element of RAT+

{ b

( not b

t2 + {} is Element of RAT+

numerator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t2),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set

denominator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator {}),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator t2),(denominator {})),K73((numerator {}),(denominator t2))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator t2),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator t2),(denominator {})),K73((numerator {}),(denominator t2))) / K73((denominator t2),(denominator {})) is Element of RAT+

xx is Element of RAT+

xx + {} is Element of RAT+

numerator xx is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator xx),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set

denominator xx is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator {}),(denominator xx)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator xx),(denominator {})),K73((numerator {}),(denominator xx))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator xx),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator xx),(denominator {})),K73((numerator {}),(denominator xx))) / K73((denominator xx),(denominator {})) is Element of RAT+

rr is Element of RAT+

xx + rr is Element of RAT+

numerator xx is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator rr is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator xx),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

numerator rr is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator xx is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator rr),(denominator xx)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator xx),(denominator rr)),K73((numerator rr),(denominator xx))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator xx),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator xx),(denominator rr)),K73((numerator rr),(denominator xx))) / K73((denominator xx),(denominator rr)) is Element of RAT+

{} *' rr is Element of RAT+

K73((numerator {}),(numerator rr)) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator {}),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator {}),(numerator rr)) / K73((denominator {}),(denominator rr)) is Element of RAT+

n0 is Element of RAT+

n0 *' rr is Element of RAT+

numerator n0 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator n0),(numerator rr)) is epsilon-transitive epsilon-connected ordinal natural set

denominator n0 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator n0),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator n0),(numerator rr)) / K73((denominator n0),(denominator rr)) is Element of RAT+

n1 is Element of RAT+

n1 *' rr is Element of RAT+

numerator n1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator n1),(numerator rr)) is epsilon-transitive epsilon-connected ordinal natural set

denominator n1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator n1),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator n1),(numerator rr)) / K73((denominator n1),(denominator rr)) is Element of RAT+

n1 + one is Element of RAT+

denominator one is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator n1),(denominator one)) is epsilon-transitive epsilon-connected ordinal natural set

numerator one is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator one),(denominator n1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator n1),(denominator one)),K73((numerator one),(denominator n1))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator n1),(denominator one)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator n1),(denominator one)),K73((numerator one),(denominator n1))) / K73((denominator n1),(denominator one)) is Element of RAT+

(n1 + one) *' rr is Element of RAT+

numerator (n1 + one) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator (n1 + one)),(numerator rr)) is epsilon-transitive epsilon-connected ordinal natural set

denominator (n1 + one) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((denominator (n1 + one)),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator (n1 + one)),(numerator rr)) / K73((denominator (n1 + one)),(denominator rr)) is Element of RAT+

(n1 *' rr) + rr is Element of RAT+

numerator (n1 *' rr) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator (n1 *' rr)),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

denominator (n1 *' rr) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator rr),(denominator (n1 *' rr))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (n1 *' rr)),(denominator rr)),K73((numerator rr),(denominator (n1 *' rr)))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator (n1 *' rr)),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (n1 *' rr)),(denominator rr)),K73((numerator rr),(denominator (n1 *' rr)))) / K73((denominator (n1 *' rr)),(denominator rr)) is Element of RAT+

s0 is Element of RAT+

((n1 *' rr) + rr) + s0 is Element of RAT+

numerator ((n1 *' rr) + rr) is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator s0 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator ((n1 *' rr) + rr)),(denominator s0)) is epsilon-transitive epsilon-connected ordinal natural set

numerator s0 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator ((n1 *' rr) + rr) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator s0),(denominator ((n1 *' rr) + rr))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator ((n1 *' rr) + rr)),(denominator s0)),K73((numerator s0),(denominator ((n1 *' rr) + rr)))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator ((n1 *' rr) + rr)),(denominator s0)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator ((n1 *' rr) + rr)),(denominator s0)),K73((numerator s0),(denominator ((n1 *' rr) + rr)))) / K73((denominator ((n1 *' rr) + rr)),(denominator s0)) is Element of RAT+

(n1 *' rr) + s0 is Element of RAT+

K73((numerator (n1 *' rr)),(denominator s0)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator s0),(denominator (n1 *' rr))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (n1 *' rr)),(denominator s0)),K73((numerator s0),(denominator (n1 *' rr)))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator (n1 *' rr)),(denominator s0)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (n1 *' rr)),(denominator s0)),K73((numerator s0),(denominator (n1 *' rr)))) / K73((denominator (n1 *' rr)),(denominator s0)) is Element of RAT+

one *' rr is Element of RAT+

K73((numerator one),(numerator rr)) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator one),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

K73((numerator one),(numerator rr)) / K73((denominator one),(denominator rr)) is Element of RAT+

(n1 *' rr) + (one *' rr) is Element of RAT+

denominator (one *' rr) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator (n1 *' rr)),(denominator (one *' rr))) is epsilon-transitive epsilon-connected ordinal natural set

numerator (one *' rr) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator (one *' rr)),(denominator (n1 *' rr))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (n1 *' rr)),(denominator (one *' rr))),K73((numerator (one *' rr)),(denominator (n1 *' rr)))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator (n1 *' rr)),(denominator (one *' rr))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator (n1 *' rr)),(denominator (one *' rr))),K73((numerator (one *' rr)),(denominator (n1 *' rr)))) / K73((denominator (n1 *' rr)),(denominator (one *' rr))) is Element of RAT+

((n1 *' rr) + s0) + rr is Element of RAT+

numerator ((n1 *' rr) + s0) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator ((n1 *' rr) + s0)),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

denominator ((n1 *' rr) + s0) is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator rr),(denominator ((n1 *' rr) + s0))) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator ((n1 *' rr) + s0)),(denominator rr)),K73((numerator rr),(denominator ((n1 *' rr) + s0)))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator ((n1 *' rr) + s0)),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator ((n1 *' rr) + s0)),(denominator rr)),K73((numerator rr),(denominator ((n1 *' rr) + s0)))) / K73((denominator ((n1 *' rr) + s0)),(denominator rr)) is Element of RAT+

xx is Element of RAT+

rr is Element of RAT+

xx + rr is Element of RAT+

numerator xx is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator rr is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator xx),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

numerator rr is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator xx is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator rr),(denominator xx)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator xx),(denominator rr)),K73((numerator rr),(denominator xx))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator xx),(denominator rr)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator xx),(denominator rr)),K73((numerator rr),(denominator xx))) / K73((denominator xx),(denominator rr)) is Element of RAT+

n0 is Element of RAT+

n1 is Element of RAT+

n1 + n0 is Element of RAT+

numerator n1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator n0 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator n1),(denominator n0)) is epsilon-transitive epsilon-connected ordinal natural set

numerator n0 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator n1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator n0),(denominator n1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator n1),(denominator n0)),K73((numerator n0),(denominator n1))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator n1),(denominator n0)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator n1),(denominator n0)),K73((numerator n0),(denominator n1))) / K73((denominator n1),(denominator n0)) is Element of RAT+

t1 is Element of RAT+

s is set

t1 is Element of RAT+

t2 is Element of RAT+

t1 + t2 is Element of RAT+

numerator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t1),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set

numerator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t2),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator t1),(denominator t2)),K73((numerator t2),(denominator t1))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator t1),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator t1),(denominator t2)),K73((numerator t2),(denominator t1))) / K73((denominator t1),(denominator t2)) is Element of RAT+

dr is Element of RAT+

xx is Element of RAT+

rr is Element of RAT+

xx + dr is Element of RAT+

numerator xx is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator xx),(denominator dr)) is epsilon-transitive epsilon-connected ordinal natural set

numerator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator xx is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator dr),(denominator xx)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator xx),(denominator dr)),K73((numerator dr),(denominator xx))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator xx),(denominator dr)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator xx),(denominator dr)),K73((numerator dr),(denominator xx))) / K73((denominator xx),(denominator dr)) is Element of RAT+

dr is Element of RAT+

xx is Element of RAT+

dr + t2 is Element of RAT+

numerator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator dr),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set

denominator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator t2),(denominator dr)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator dr),(denominator t2)),K73((numerator t2),(denominator dr))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator dr),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator dr),(denominator t2)),K73((numerator t2),(denominator dr))) / K73((denominator dr),(denominator t2)) is Element of RAT+

rone is Element of ()

(rone) is Element of ()

x is Element of ()

(x) is Element of ()

rone is Element of ()

x is Element of ()

(rone,x) is Element of ()

y is Element of ()

(rone,y) is Element of ()

(rone) is Element of ()

(x) is Element of ()

y is Element of ()

((rone),y) is Element of ()

{ (b

(y) is Element of ()

(rone,(y)) is Element of ()

{ (b

y9 is set

A is Element of RAT+

B is Element of RAT+

A + B is Element of RAT+

numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator A),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator B),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator A),(denominator B)),K73((numerator B),(denominator A))) is epsilon-transitive epsilon-connected ordinal natural set

K73((denominator A),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((numerator A),(denominator B)),K73((numerator B),(denominator A))) / K73((denominator A),(denominator B)) is Element of RAT+

((y)) is Element of ()

((rone),((y))) is Element of ()

{ (b

(((rone),((y)))) is Element of ()

((x)) is Element of ()

rone is Element of ()

x is Element of ()

rone is Element of ()

x is Element of ()

(rone,x) is Element of ()

y is Element of ()

(rone,y) is Element of ()

y9 is Element of ()

(y,y9) is Element of ()

(x,y9) is Element of ()

((rone,x),y9) is Element of ()

((rone,y),y9) is Element of ()

rone is Element of ()

x is Element of ()

y is Element of ()

(x,y) is Element of ()

{ (b

(rone,(x,y)) is Element of ()

{ (b

(rone,x) is Element of ()

{ (b

((rone,x),y) is Element of ()

{ (b

y9 is set

A is Element of RAT+

B is Element of RAT+

A *' B is Element of RAT+

numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega

numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega

K73((numerator A),(numerator B)) is epsilon-transitive epsilon-connected ordinal natural set

denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega