:: 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₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural Element of omega
{ [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is Element of bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) }
bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is non empty set
( { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } ) \/ omega is non empty set
{} 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₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } is set
{RAT+} is non empty set
{ b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } \ {RAT+} is Element of bool { b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) }
bool { b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } is non empty set
bool (bool RAT+) is non empty set
RA is set
rone is Element of bool RAT+
() is Element of bool (bool RAT+)
{ b₁ where b₁ is Element of RAT+ : not one <=' b₁ } is set
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₂ where b₂ is Element of RAT+ : not b₁ <=' b₂ } where b₁ is Element of RAT+ : not b₁ = {} } is set
(RAT+ \/ ()) \ { { b₂ where b₂ is Element of RAT+ : not b₁ <=' b₂ } where b₁ is Element of RAT+ : not b₁ = {} } is Element of bool (RAT+ \/ ())
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₁ where b₁ is Element of RAT+ : not x <=' b₁ } is set
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₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } is non empty set
( { b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } \ {RAT+}) \ { { b₂ where b₂ is Element of RAT+ : not b₁ <=' b₂ } where b₁ is Element of RAT+ : not b₁ = {} } is Element of bool { b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) }
RAT+ \/ (( { b₁ where b₁ is Element of bool RAT+ : for b₂ being Element of RAT+ holds
( not b₂ in b₁ or ( ( for b₃ being Element of RAT+ holds
( not b₃ <=' b₂ or b₃ in b₁ ) ) & ex b₃ being Element of RAT+ st
( b₃ in b₁ & not b₃ <=' b₂ ) ) ) } \ {RAT+}) \ { { b₂ where b₂ is Element of RAT+ : not b₁ <=' b₂ } where b₁ is Element of RAT+ : not b₁ = {} } ) is non empty set
() \ { { b₂ where b₂ is Element of RAT+ : not b₁ <=' b₂ } where b₁ is Element of RAT+ : not b₁ = {} } is Element of bool (bool RAT+)
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is Element of bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) }
bool { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } is non empty set
( { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b₁,b₂ are_relative_prime & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } ) \/ omega is non empty set
rone is Element of ()
x is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not x <=' b₁ } is set
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₁ where b₁ is Element of RAT+ : not y9 <=' b₁ } is set
A is Element of RAT+
y is Element of ()
{ b₁ where b₁ is Element of RAT+ : not A <=' b₁ } is set
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₁ where b₁ is Element of RAT+ : not x <=' b₁ } is set
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₁ where b₁ is Element of RAT+ : not {} <=' b₁ } is set
x is set
y is Element of RAT+
x is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not x <=' b₁ } is set
x is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not x <=' b₁ } is set
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₁ where b₁ is Element of RAT+ : not y <=' b₁ } is set
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₁ where b₁ is Element of RAT+ : not rone <=' b₁ } is set
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₁ where b₁ is Element of RAT+ : not y <=' b₁ } is set
y9 is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not y9 <=' b₁ } is set
A is Element of RAT+
y is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not y <=' b₁ } is set
y9 is Element of RAT+
y is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not y <=' b₁ } is set
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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in x ) } is set
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₂) where b₁, b₂ is Element of RAT+ : ( b₁ in y9 & b₂ in A ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in A & b₂ in y9 ) } is set
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₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in x ) } is set
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₂) where b₁, b₂ is Element of RAT+ : ( b₁ in y9 & b₂ in A ) } is set
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in A & b₂ in y9 ) } is set
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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in (x) ) } is set
(((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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (y9) & b₂ in (A) ) } is set
(((y9),(A))) is Element of ()
((A),(y9)) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (A) & b₂ in (y9) ) } is set
(((A),(y9))) is Element of ()
((rone),(x)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in (x) ) } is set
(((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₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (y9) & b₂ in (A) ) } is set
(((y9),(A))) is Element of ()
((A),(y9)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (A) & b₂ in (y9) ) } is set
(((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₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in (x) ) } is set
(((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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in (x) ) } is set
((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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in x & b₂ in y ) } is set
(rone,(x,y)) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in (x,y) ) } is set
(rone,x) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in x ) } is set
((rone,x),y) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone,x) & b₂ in y ) } is set
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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in x & b₂ in y ) } is set
(rone,(x,y)) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in (x,y) ) } is set
(rone,x) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in x ) } is set
((rone,x),y) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone,x) & b₂ in y ) } is set
rone is Element of ()
x is Element of ()
(rone,x) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in x ) } is set
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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (x) & b₂ in (y) ) } is set
(((x),(y))) is Element of ()
(rone) is Element of ()
((rone),(x)) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in (x) ) } is set
(((rone),(x))) is Element of ()
(rone,(((x),(y)))) is Element of ()
((((x),(y)))) is Element of ()
((rone),((((x),(y))))) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in ((((x),(y)))) ) } is set
(((rone),((((x),(y)))))) is Element of ()
((rone),((x),(y))) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in ((x),(y)) ) } is set
(((rone),((x),(y)))) is Element of ()
(((rone),(x)),(y)) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in ((rone),(x)) & b₂ in (y) ) } is set
((((rone),(x)),(y))) is Element of ()
((((rone),(x)))) is Element of ()
(((((rone),(x)))),(y)) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in ((((rone),(x)))) & b₂ in (y) ) } is set
((((((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₁ where b₁ is Element of RAT+ : not y <=' b₁ } is set
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₁ where b₁ is Element of RAT+ : ex b₂, b₃ being Element of () st
( b₃ = b₁ & b₂ in rone & (b₂,b₃) ) } is set
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₁ where b₁ is Element of RAT+ : not A <=' b₁ } is set
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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in x ) } is set
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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in (x) ) } is set
(((rone),(x))) is Element of ()
((((rone),(x)))) is Element of ()
rone is Element of ()
x is Element of ()
y is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : ex b₂, b₃ being Element of RAT+ st
( not b₂ in rone & b₃ in x & b₂ + b₁ = b₃ ) } is set
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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in x9 ) } is set
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₁ where b₁ is Element of RAT+ : ex b₂ being Element of RAT+ st
( not b₂ in rone & b₂ + b₁ = t2 ) } is set
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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in y ) } is set
(y) is Element of ()
(rone,(y)) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in y & b₂ in (rone) ) } is set
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₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in ((y)) ) } is set
(((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₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in x & b₂ in y ) } is set
(rone,(x,y)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in (x,y) ) } is set
(rone,x) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in x ) } is set
((rone,x),y) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone,x) & b₂ in y ) } is set
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+
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+
A *' x9 is Element of RAT+
K73((numerator A),(numerator x9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator A),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator A),(numerator x9)) / 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)),(numerator r)) is epsilon-transitive epsilon-connected ordinal natural set
denominator (A *' x9) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator (A *' x9)),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator (A *' x9)),(numerator r)) / 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₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in x & b₂ in y ) } is set
(rone,(x,y)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in (x,y) ) } is set
(rone,x) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in x ) } is set
((rone,x),y) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone,x) & b₂ in y ) } is set
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₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in (x) ) } is set
(((rone),(x))) is Element of ()
y is Element of ()
(x,y) is Element of ()
(y) is Element of ()
((x),(y)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (x) & b₂ in (y) ) } is set
(((x),(y))) is Element of ()
(rone,(x,y)) is Element of ()
((x,y)) is Element of ()
((rone),((x,y))) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in ((x,y)) ) } is set
(((rone),((x,y)))) is Element of ()
((rone,x),y) is Element of ()
((rone,x)) is Element of ()
(((rone,x)),(y)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in ((rone,x)) & b₂ in (y) ) } is set
((((rone,x)),(y))) is Element of ()
((rone),((x),(y))) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in ((x),(y)) ) } is set
(((rone),((x),(y)))) is Element of ()
(((rone),(x)),(y)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in ((rone),(x)) & b₂ in (y) ) } is set
((((rone),(x)),(y))) 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₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in (x) ) } is set
(((rone),(x))) is Element of ()
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
numerator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator y),(numerator y9)) is epsilon-transitive epsilon-connected ordinal natural set
denominator y is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator y),(denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator y),(numerator y9)) / K73((denominator y),(denominator y9)) is Element of RAT+
rone is Element of ()
x is Element of ()
y is Element of ()
(x,y) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in x & b₂ in y ) } is set
(rone,(x,y)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in (x,y) ) } is set
(rone,x) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in x ) } is set
(rone,y) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in rone & b₂ in y ) } is set
((rone,x),(rone,y)) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone,x) & b₂ in (rone,y) ) } is set
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+
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),(numerator x9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator A),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator A),(numerator x9)) / K73((denominator A),(denominator x9)) is Element of RAT+
A *' r is Element of RAT+
K73((numerator A),(numerator r)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator A),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator A),(numerator r)) / K73((denominator A),(denominator r)) is Element of RAT+
(A *' x9) + (A *' r) is Element of RAT+
numerator (A *' x9) is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator (A *' r) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (A *' x9)),(denominator (A *' r))) is epsilon-transitive epsilon-connected ordinal natural set
numerator (A *' r) is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator (A *' x9) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (A *' r)),(denominator (A *' x9))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (A *' x9)),(denominator (A *' r))),K73((numerator (A *' r)),(denominator (A *' x9)))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator (A *' x9)),(denominator (A *' r))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (A *' x9)),(denominator (A *' r))),K73((numerator (A *' r)),(denominator (A *' x9)))) / K73((denominator (A *' x9)),(denominator (A *' r))) 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
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
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+
s *' r is Element of RAT+
K73((numerator s),(numerator r)) is epsilon-transitive epsilon-connected ordinal natural set
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+
t2 is Element of RAT+
s *' t2 is Element of RAT+
numerator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator s),(numerator t2)) is epsilon-transitive epsilon-connected ordinal natural set
denominator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator s),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator s),(numerator t2)) / K73((denominator s),(denominator t2)) is Element of RAT+
t2 + t1 is Element of RAT+
K73((numerator t2),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator t1),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set
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 *' (t2 + t1) is Element of RAT+
numerator (t2 + t1) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator s),(numerator (t2 + t1))) is epsilon-transitive epsilon-connected ordinal natural set
denominator (t2 + t1) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator s),(denominator (t2 + t1))) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator s),(numerator (t2 + t1))) / K73((denominator s),(denominator (t2 + t1))) is Element of RAT+
x9 *' t1 is Element of RAT+
K73((numerator x9),(numerator t1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator x9),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator x9),(numerator t1)) / K73((denominator x9),(denominator t1)) is Element of RAT+
t2 is Element of RAT+
x9 *' t2 is Element of RAT+
numerator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator x9),(numerator t2)) is epsilon-transitive epsilon-connected ordinal natural set
denominator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator x9),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator x9),(numerator t2)) / K73((denominator x9),(denominator t2)) is Element of RAT+
r + t2 is Element of RAT+
K73((numerator r),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator t2),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator r),(denominator t2)),K73((numerator t2),(denominator r))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator r),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator r),(denominator t2)),K73((numerator t2),(denominator r))) / K73((denominator r),(denominator t2)) is Element of RAT+
x9 *' (r + t2) is Element of RAT+
numerator (r + t2) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator x9),(numerator (r + t2))) is epsilon-transitive epsilon-connected ordinal natural set
denominator (r + t2) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator x9),(denominator (r + t2))) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator x9),(numerator (r + t2))) / K73((denominator x9),(denominator (r + t2))) 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₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in (x) ) } is set
(((rone),(x))) is Element of ()
y is Element of ()
(x,y) is Element of ()
(rone,(x,y)) is Element of ()
((x,y)) is Element of ()
((rone),((x,y))) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in ((x,y)) ) } is set
(((rone),((x,y)))) is Element of ()
(rone,y) is Element of ()
(y) is Element of ()
((rone),(y)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in (y) ) } is set
(((rone),(y))) is Element of ()
((rone,x),(rone,y)) is Element of ()
(rone,rone) is Element of ()
(rone,(rone,y)) is Element of ()
(x,(rone,y)) is Element of ()
((rone,x),y) is Element of ()
((x),(y)) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (x) & b₂ in (y) ) } is set
(((x),(y))) is Element of ()
((((x),(y)))) is Element of ()
((rone),((((x),(y))))) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in ((((x),(y)))) ) } is set
(((rone),((((x),(y)))))) is Element of ()
((rone),((x),(y))) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (rone) & b₂ in ((x),(y)) ) } is set
(((rone),((x),(y)))) is Element of ()
(((rone),(x)),((rone),(y))) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in ((rone),(x)) & b₂ in ((rone),(y)) ) } is set
((((rone),(x)),((rone),(y)))) is Element of ()
((rone,y)) is Element of ()
(((rone),(x)),((rone,y))) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in ((rone),(x)) & b₂ in ((rone,y)) ) } is set
((((rone),(x)),((rone,y)))) is Element of ()
((rone,x)) is Element of ()
(((rone,x)),((rone,y))) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in ((rone,x)) & b₂ in ((rone,y)) ) } is set
((((rone,x)),((rone,y)))) is Element of ()
x is set
y is 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 ()
(rone) is Element of ()
x is Element of ()
y is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not y <=' b₁ } is set
y9 is Element of RAT+
y *' y9 is Element of RAT+
numerator y is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator y),(numerator y9)) is epsilon-transitive epsilon-connected ordinal natural set
denominator y is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator y),(denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator y),(numerator y9)) / K73((denominator y),(denominator y9)) is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not y9 <=' b₁ } is set
B is set
x9 is Element of RAT+
B is Element of bool RAT+
x9 is Element of RAT+
r is Element of RAT+
r is Element of RAT+
s is Element of RAT+
t1 is Element of RAT+
x9 is Element of RAT+
x9 is Element of ()
(x,x9) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in x & b₂ in x9 ) } is set
{ b₁ where b₁ is Element of RAT+ : not y *' y9 <=' b₁ } is set
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
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+
y *' t1 is Element of RAT+
K73((numerator y),(numerator t1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator y),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator y),(numerator t1)) / K73((denominator y),(denominator t1)) is Element of RAT+
t2 is Element of RAT+
t2 is Element of RAT+
t2 is Element of RAT+
r is set
s is Element of RAT+
t1 is Element of RAT+
y *' t1 is Element of RAT+
numerator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator y),(numerator t1)) is epsilon-transitive epsilon-connected ordinal natural set
denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator y),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator y),(numerator t1)) / K73((denominator y),(denominator t1)) is Element of RAT+
t2 is Element of RAT+
t2 *' y is Element of RAT+
numerator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator t2),(numerator y)) is epsilon-transitive epsilon-connected ordinal natural set
denominator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator t2),(denominator y)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator t2),(numerator y)) / K73((denominator t2),(denominator y)) is Element of RAT+
dr is Element of RAT+
t2 *' dr is Element of RAT+
numerator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator t2),(numerator dr)) is epsilon-transitive epsilon-connected ordinal natural set
denominator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator t2),(denominator dr)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator t2),(numerator dr)) / K73((denominator t2),(denominator dr)) is Element of RAT+
r is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not r <=' b₁ } is set
{ b₁ where b₁ is Element of RAT+ : ex b₂ being Element of RAT+ st
( not b₂ in x & b₂ *' b₁ <=' one ) } is set
y9 is set
A is Element of RAT+
B is Element of RAT+
B *' A is Element of RAT+
numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator B),(numerator A)) is epsilon-transitive epsilon-connected ordinal natural set
denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator B),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator B),(numerator A)) / K73((denominator B),(denominator A)) is Element of RAT+
y9 is Element of RAT+
y9 *' {} is Element of RAT+
numerator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator y9),(numerator {})) is epsilon-transitive epsilon-connected ordinal natural set
denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator y9),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator y9),(numerator {})) / K73((denominator y9),(denominator {})) is Element of RAT+
B 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+
r *' x9 is Element of RAT+
numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator r),(numerator x9)) is epsilon-transitive epsilon-connected ordinal natural set
denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator r),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator r),(numerator x9)) / K73((denominator r),(denominator x9)) is Element of RAT+
x9 is Element of RAT+
x9 *' B is Element of RAT+
numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator x9),(numerator B)) is epsilon-transitive epsilon-connected ordinal natural set
denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator x9),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator x9),(numerator B)) / K73((denominator x9),(denominator B)) is Element of RAT+
r is Element of RAT+
x9 *' r is Element of RAT+
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 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+
r is Element of RAT+
s is Element of RAT+
r *' s is Element of RAT+
numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator s is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator r),(numerator s)) is epsilon-transitive epsilon-connected ordinal natural set
denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator s is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator r),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator r),(numerator s)) / K73((denominator r),(denominator s)) is Element of RAT+
r *' B is Element of RAT+
K73((numerator r),(numerator B)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator r),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator r),(numerator B)) / K73((denominator r),(denominator B)) is Element of RAT+
x9 *' s is Element of RAT+
K73((numerator x9),(numerator s)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator x9),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator x9),(numerator s)) / K73((denominator x9),(denominator s)) 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+
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+
r is Element of ()
(x,r) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in x & b₂ in r ) } is set
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
numerator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator t1),(numerator t2)) is epsilon-transitive epsilon-connected ordinal natural set
denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator t1),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator t1),(numerator t2)) / K73((denominator t1),(denominator t2)) is Element of RAT+
dr is Element of RAT+
xx is Element of RAT+
xx *' dr is Element of RAT+
numerator xx is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator xx),(numerator dr)) is epsilon-transitive epsilon-connected ordinal natural set
denominator xx is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator xx),(denominator dr)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator xx),(numerator dr)) / K73((denominator xx),(denominator dr)) is Element of RAT+
dr 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),(numerator t2)) is epsilon-transitive epsilon-connected ordinal natural set
denominator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator dr),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator dr),(numerator t2)) / K73((denominator dr),(denominator t2)) is Element of RAT+
{} *' {} is Element of RAT+
K73((numerator {}),(numerator {})) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator {}),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator {}),(numerator {})) / K73((denominator {}),(denominator {})) 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+
{ (s *' b₁) where b₁ is Element of RAT+ : b₁ in x } is set
t2 is set
dr is Element of RAT+
s *' dr is Element of RAT+
numerator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator s),(numerator dr)) is epsilon-transitive epsilon-connected ordinal natural set
denominator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator s),(denominator dr)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator s),(numerator dr)) / K73((denominator s),(denominator dr)) is Element of RAT+
dr is Element of RAT+
s + dr is Element of RAT+
denominator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator s),(denominator dr)) is epsilon-transitive epsilon-connected ordinal natural set
numerator dr is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator dr),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator s),(denominator dr)),K73((numerator dr),(denominator s))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator s),(denominator dr)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator s),(denominator dr)),K73((numerator dr),(denominator s))) / K73((denominator s),(denominator dr)) is Element of RAT+
xx is Element of RAT+
B *' dr is Element of RAT+
K73((numerator B),(numerator dr)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator B),(denominator dr)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator B),(numerator dr)) / K73((denominator B),(denominator dr)) is Element of RAT+
n0 is Element of RAT+
n0 *' (B *' dr) is Element of RAT+
numerator n0 is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator (B *' dr) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator n0),(numerator (B *' dr))) is epsilon-transitive epsilon-connected ordinal natural set
denominator n0 is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator (B *' dr) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator n0),(denominator (B *' dr))) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator n0),(numerator (B *' dr))) / K73((denominator n0),(denominator (B *' dr))) is Element of RAT+
{} *' (B *' dr) is Element of RAT+
K73((numerator {}),(numerator (B *' dr))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator {}),(denominator (B *' dr))) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator {}),(numerator (B *' dr))) / K73((denominator {}),(denominator (B *' dr))) is Element of RAT+
n1 is Element of RAT+
n1 *' (B *' dr) is Element of RAT+
numerator n1 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator n1),(numerator (B *' dr))) is epsilon-transitive epsilon-connected ordinal natural set
denominator n1 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator n1),(denominator (B *' dr))) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator n1),(numerator (B *' dr))) / K73((denominator n1),(denominator (B *' dr))) 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) *' (B *' dr) is Element of RAT+
numerator (n1 + one) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (n1 + one)),(numerator (B *' dr))) 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 (B *' dr))) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator (n1 + one)),(numerator (B *' dr))) / K73((denominator (n1 + one)),(denominator (B *' dr))) is Element of RAT+
t2 is Element of bool RAT+
s9 is Element of RAT+
s *' s9 is Element of RAT+
numerator s9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator s),(numerator s9)) is epsilon-transitive epsilon-connected ordinal natural set
denominator s9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator s),(denominator s9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator s),(numerator s9)) / K73((denominator s),(denominator s9)) is Element of RAT+
one *' (B *' dr) is Element of RAT+
K73((numerator one),(numerator (B *' dr))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator one),(denominator (B *' dr))) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator one),(numerator (B *' dr))) / K73((denominator one),(denominator (B *' dr))) is Element of RAT+
(n1 *' (B *' dr)) + (one *' (B *' dr)) is Element of RAT+
numerator (n1 *' (B *' dr)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator (one *' (B *' dr)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (n1 *' (B *' dr))),(denominator (one *' (B *' dr)))) is epsilon-transitive epsilon-connected ordinal natural set
numerator (one *' (B *' dr)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator (n1 *' (B *' dr)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (one *' (B *' dr))),(denominator (n1 *' (B *' dr)))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (n1 *' (B *' dr))),(denominator (one *' (B *' dr)))),K73((numerator (one *' (B *' dr))),(denominator (n1 *' (B *' dr))))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator (n1 *' (B *' dr))),(denominator (one *' (B *' dr)))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (n1 *' (B *' dr))),(denominator (one *' (B *' dr)))),K73((numerator (one *' (B *' dr))),(denominator (n1 *' (B *' dr))))) / K73((denominator (n1 *' (B *' dr))),(denominator (one *' (B *' dr)))) is Element of RAT+
dr *' B is Element of RAT+
K73((numerator dr),(numerator B)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator dr),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator dr),(numerator B)) / K73((denominator dr),(denominator B)) is Element of RAT+
(s *' s9) + (dr *' B) is Element of RAT+
numerator (s *' s9) is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator (dr *' B) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (s *' s9)),(denominator (dr *' B))) is epsilon-transitive epsilon-connected ordinal natural set
numerator (dr *' B) is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator (s *' s9) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (dr *' B)),(denominator (s *' s9))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (s *' s9)),(denominator (dr *' B))),K73((numerator (dr *' B)),(denominator (s *' s9)))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator (s *' s9)),(denominator (dr *' B))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (s *' s9)),(denominator (dr *' B))),K73((numerator (dr *' B)),(denominator (s *' s9)))) / K73((denominator (s *' s9)),(denominator (dr *' B))) is Element of RAT+
s1 is Element of RAT+
dr *' s1 is Element of RAT+
numerator s1 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator dr),(numerator s1)) is epsilon-transitive epsilon-connected ordinal natural set
denominator s1 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator dr),(denominator s1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator dr),(numerator s1)) / K73((denominator dr),(denominator s1)) is Element of RAT+
s *' s1 is Element of RAT+
K73((numerator s),(numerator s1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator s),(denominator s1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator s),(numerator s1)) / K73((denominator s),(denominator s1)) is Element of RAT+
(s *' s1) + (dr *' B) is Element of RAT+
numerator (s *' s1) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (s *' s1)),(denominator (dr *' B))) is epsilon-transitive epsilon-connected ordinal natural set
denominator (s *' s1) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (dr *' B)),(denominator (s *' s1))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (s *' s1)),(denominator (dr *' B))),K73((numerator (dr *' B)),(denominator (s *' s1)))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator (s *' s1)),(denominator (dr *' B))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (s *' s1)),(denominator (dr *' B))),K73((numerator (dr *' B)),(denominator (s *' s1)))) / K73((denominator (s *' s1)),(denominator (dr *' B))) is Element of RAT+
(s *' s1) + (dr *' s1) is Element of RAT+
denominator (dr *' s1) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (s *' s1)),(denominator (dr *' s1))) is epsilon-transitive epsilon-connected ordinal natural set
numerator (dr *' s1) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (dr *' s1)),(denominator (s *' s1))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (s *' s1)),(denominator (dr *' s1))),K73((numerator (dr *' s1)),(denominator (s *' s1)))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator (s *' s1)),(denominator (dr *' s1))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (s *' s1)),(denominator (dr *' s1))),K73((numerator (dr *' s1)),(denominator (s *' s1)))) / K73((denominator (s *' s1)),(denominator (dr *' s1))) is Element of RAT+
(s + dr) *' s1 is Element of RAT+
numerator (s + dr) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (s + dr)),(numerator s1)) is epsilon-transitive epsilon-connected ordinal natural set
denominator (s + dr) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator (s + dr)),(denominator s1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator (s + dr)),(numerator s1)) / K73((denominator (s + dr)),(denominator s1)) is Element of RAT+
(n1 *' (B *' dr)) *' t1 is Element of RAT+
K73((numerator (n1 *' (B *' dr))),(numerator t1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator (n1 *' (B *' dr))),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator (n1 *' (B *' dr))),(numerator t1)) / K73((denominator (n1 *' (B *' dr))),(denominator t1)) is Element of RAT+
s *' ((n1 *' (B *' dr)) *' t1) is Element of RAT+
numerator ((n1 *' (B *' dr)) *' t1) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator s),(numerator ((n1 *' (B *' dr)) *' t1))) is epsilon-transitive epsilon-connected ordinal natural set
denominator ((n1 *' (B *' dr)) *' t1) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator s),(denominator ((n1 *' (B *' dr)) *' t1))) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator s),(numerator ((n1 *' (B *' dr)) *' t1))) / K73((denominator s),(denominator ((n1 *' (B *' dr)) *' t1))) is Element of RAT+
one *' (n1 *' (B *' dr)) is Element of RAT+
K73((numerator one),(numerator (n1 *' (B *' dr)))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator one),(denominator (n1 *' (B *' dr)))) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator one),(numerator (n1 *' (B *' dr)))) / K73((denominator one),(denominator (n1 *' (B *' dr)))) is Element of RAT+
s *' {} is Element of RAT+
K73((numerator s),(numerator {})) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator s),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator s),(numerator {})) / K73((denominator s),(denominator {})) is Element of RAT+
s9 is Element of RAT+
(n1 *' (B *' dr)) *' s9 is Element of RAT+
numerator s9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (n1 *' (B *' dr))),(numerator s9)) is epsilon-transitive epsilon-connected ordinal natural set
denominator s9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator (n1 *' (B *' dr))),(denominator s9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator (n1 *' (B *' dr))),(numerator s9)) / K73((denominator (n1 *' (B *' dr))),(denominator s9)) is Element of RAT+
s *' s9 is Element of RAT+
K73((numerator s),(numerator s9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator s),(denominator s9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator s),(numerator s9)) / K73((denominator s),(denominator s9)) is Element of RAT+
(n1 *' (B *' dr)) *' (s *' s9) is Element of RAT+
numerator (s *' s9) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (n1 *' (B *' dr))),(numerator (s *' s9))) is epsilon-transitive epsilon-connected ordinal natural set
denominator (s *' s9) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator (n1 *' (B *' dr))),(denominator (s *' s9))) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator (n1 *' (B *' dr))),(numerator (s *' s9))) / K73((denominator (n1 *' (B *' dr))),(denominator (s *' s9))) is Element of RAT+
((n1 *' (B *' dr)) *' s9) *' s is Element of RAT+
numerator ((n1 *' (B *' dr)) *' s9) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator ((n1 *' (B *' dr)) *' s9)),(numerator s)) is epsilon-transitive epsilon-connected ordinal natural set
denominator ((n1 *' (B *' dr)) *' s9) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator ((n1 *' (B *' dr)) *' s9)),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator ((n1 *' (B *' dr)) *' s9)),(numerator s)) / K73((denominator ((n1 *' (B *' dr)) *' s9)),(denominator s)) is Element of RAT+
((n1 *' (B *' dr)) *' t1) *' (s *' s9) is Element of RAT+
K73((numerator ((n1 *' (B *' dr)) *' t1)),(numerator (s *' s9))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator ((n1 *' (B *' dr)) *' t1)),(denominator (s *' s9))) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator ((n1 *' (B *' dr)) *' t1)),(numerator (s *' s9))) / K73((denominator ((n1 *' (B *' dr)) *' t1)),(denominator (s *' s9))) is Element of RAT+
((n1 *' (B *' dr)) *' t1) *' s is Element of RAT+
K73((numerator ((n1 *' (B *' dr)) *' t1)),(numerator s)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator ((n1 *' (B *' dr)) *' t1)),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator ((n1 *' (B *' dr)) *' t1)),(numerator s)) / K73((denominator ((n1 *' (B *' dr)) *' t1)),(denominator s)) is Element of RAT+
(((n1 *' (B *' dr)) *' t1) *' s) *' s9 is Element of RAT+
numerator (((n1 *' (B *' dr)) *' t1) *' s) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator (((n1 *' (B *' dr)) *' t1) *' s)),(numerator s9)) is epsilon-transitive epsilon-connected ordinal natural set
denominator (((n1 *' (B *' dr)) *' t1) *' s) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator (((n1 *' (B *' dr)) *' t1) *' s)),(denominator s9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator (((n1 *' (B *' dr)) *' t1) *' s)),(numerator s9)) / K73((denominator (((n1 *' (B *' dr)) *' t1) *' s)),(denominator s9)) is Element of RAT+
(n1 *' (B *' dr)) *' one is Element of RAT+
K73((numerator (n1 *' (B *' dr))),(numerator one)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator (n1 *' (B *' dr))),(denominator one)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator (n1 *' (B *' dr))),(numerator one)) / K73((denominator (n1 *' (B *' dr))),(denominator one)) is Element of RAT+
((n1 *' (B *' dr)) *' one) *' s9 is Element of RAT+
numerator ((n1 *' (B *' dr)) *' one) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator ((n1 *' (B *' dr)) *' one)),(numerator s9)) is epsilon-transitive epsilon-connected ordinal natural set
denominator ((n1 *' (B *' dr)) *' one) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator ((n1 *' (B *' dr)) *' one)),(denominator s9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator ((n1 *' (B *' dr)) *' one)),(numerator s9)) / K73((denominator ((n1 *' (B *' dr)) *' one)),(denominator s9)) is Element of RAT+
((x,r)) is Element of ()
(((x,r))) is Element of ()
x is Element of ()
(x) is Element of ()
y is Element of ()
((x),y) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (x) & b₂ in y ) } is set
(y) is Element of ()
y9 is Element of ()
(x,y9) is Element of ()
(y9) is Element of ()
((x),(y9)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (x) & b₂ in (y9) ) } is set
(((x),(y9))) is Element of ()
((rone)) is Element of ()
{ b₁ where b₁ is Element of RAT+ : not one <=' b₁ } is set
x is Element of ()
y is Element of ()
(x,y) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in x & b₂ in y ) } is set
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+
one *' B is Element of RAT+
numerator one is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator one),(numerator B)) is epsilon-transitive epsilon-connected ordinal natural set
denominator one is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator one),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator one),(numerator B)) / K73((denominator one),(denominator B)) is Element of RAT+
x9 is Element of RAT+
y9 is set
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+
one *' A is Element of RAT+
numerator one is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator one),(numerator A)) is epsilon-transitive epsilon-connected ordinal natural set
denominator one is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator one),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator one),(numerator A)) / K73((denominator one),(denominator A)) is Element of RAT+
x9 *' B is Element of RAT+
K73((numerator x9),(numerator B)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator x9),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator x9),(numerator B)) / K73((denominator x9),(denominator B)) is Element of RAT+
x is Element of ()
y is Element of ()
(x,y) is Element of ()
(x) is Element of ()
(y) is Element of ()
((x),(y)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (x) & b₂ in (y) ) } is set
(((x),(y))) is Element of ()
((y)) is Element of ()
y9 is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not y9 <=' b₁ } is set
x is epsilon-transitive epsilon-connected ordinal natural Element of omega
y is epsilon-transitive epsilon-connected ordinal natural Element of omega
x +^ y is epsilon-transitive epsilon-connected ordinal natural 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
denominator A is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator y9),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set
numerator A is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator A),(denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator y9),(denominator A)),K73((numerator A),(denominator y9))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator y9),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator y9),(denominator A)),K73((numerator A),(denominator y9))) / K73((denominator y9),(denominator A)) is Element of RAT+
(denominator y9) *^ (denominator A) is epsilon-transitive epsilon-connected ordinal natural set
(numerator y9) *^ (denominator A) is epsilon-transitive epsilon-connected ordinal natural set
(numerator A) *^ (denominator y9) is epsilon-transitive epsilon-connected ordinal natural set
((numerator y9) *^ (denominator A)) +^ ((numerator A) *^ (denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set
RED (((denominator y9) *^ (denominator A)),(((numerator y9) *^ (denominator A)) +^ ((numerator A) *^ (denominator y9)))) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((denominator y9) *^ (denominator A)) hcf (((numerator y9) *^ (denominator A)) +^ ((numerator A) *^ (denominator y9))) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K70(((denominator y9) *^ (denominator A)),(((denominator y9) *^ (denominator A)) hcf (((numerator y9) *^ (denominator A)) +^ ((numerator A) *^ (denominator y9))))) is epsilon-transitive epsilon-connected ordinal natural set
(numerator y9) *^ one is epsilon-transitive epsilon-connected ordinal natural set
((numerator y9) *^ one) +^ (numerator A) is epsilon-transitive epsilon-connected ordinal natural set
(numerator y9) +^ (numerator A) is epsilon-transitive epsilon-connected ordinal natural set
x +^ (numerator A) is epsilon-transitive epsilon-connected ordinal natural set
RED ((((numerator y9) *^ (denominator A)) +^ ((numerator A) *^ (denominator y9))),((denominator y9) *^ (denominator A))) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(((numerator y9) *^ (denominator A)) +^ ((numerator A) *^ (denominator y9))) hcf ((denominator y9) *^ (denominator A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
K70((((numerator y9) *^ (denominator A)) +^ ((numerator A) *^ (denominator y9))),((((numerator y9) *^ (denominator A)) +^ ((numerator A) *^ (denominator y9))) hcf ((denominator y9) *^ (denominator A)))) is epsilon-transitive epsilon-connected ordinal natural set
x is Element of RAT+
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+
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+
{} + B is Element of RAT+
numerator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator {}),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set
denominator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator B),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator {}),(denominator B)),K73((numerator B),(denominator {}))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator {}),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator {}),(denominator B)),K73((numerator B),(denominator {}))) / K73((denominator {}),(denominator B)) is Element of RAT+
x9 is Element of RAT+
x9 + A is Element of RAT+
numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator x9),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set
denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator A),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator x9),(denominator A)),K73((numerator A),(denominator x9))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator x9),(denominator A)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator x9),(denominator A)),K73((numerator A),(denominator x9))) / K73((denominator x9),(denominator A)) is Element of RAT+
r is Element of RAT+
s is Element of RAT+
r + s is Element of RAT+
numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega
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
numerator s is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator s),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator r),(denominator s)),K73((numerator s),(denominator r))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator r),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator r),(denominator s)),K73((numerator s),(denominator r))) / K73((denominator r),(denominator s)) is Element of RAT+
s + r is Element of RAT+
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+
x is Element of ()
y is Element of ()
(x,y) is Element of ()
y9 is Element of RAT+
{} + y9 is Element of RAT+
numerator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator {}),(denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set
numerator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator y9),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator {}),(denominator y9)),K73((numerator y9),(denominator {}))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator {}),(denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator {}),(denominator y9)),K73((numerator y9),(denominator {}))) / K73((denominator {}),(denominator y9)) is Element of RAT+
y9 is Element of RAT+
y9 + {} is Element of RAT+
numerator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator y9),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set
numerator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator {}),(denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator y9),(denominator {})),K73((numerator {}),(denominator y9))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator y9),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator y9),(denominator {})),K73((numerator {}),(denominator y9))) / K73((denominator y9),(denominator {})) is Element of RAT+
(x) is Element of ()
(y) is Element of ()
B is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not B <=' b₁ } is set
x9 is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not x9 <=' b₁ } is set
((x),(y)) is Element of ()
{ (b₁ + b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (x) & b₂ in (y) ) } is set
B + x9 is Element of RAT+
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
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
K72(K73((numerator B),(denominator x9)),K73((numerator x9),(denominator B))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator B),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator B),(denominator x9)),K73((numerator x9),(denominator B))) / K73((denominator B),(denominator x9)) is Element of RAT+
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
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+
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+
t2 is Element of RAT+
t2 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+
(((x),(y))) is Element of ()
r is Element of RAT+
s is Element of RAT+
x is Element of ()
y is Element of ()
(y,x) is Element of ()
(x,y) is Element of ()
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
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
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
K72(K73((numerator B),(denominator x9)),K73((numerator x9),(denominator B))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator B),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator B),(denominator x9)),K73((numerator x9),(denominator B))) / K73((denominator B),(denominator x9)) is Element of RAT+
y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
A is epsilon-transitive epsilon-connected ordinal natural Element of omega
y9 +^ A is epsilon-transitive epsilon-connected ordinal natural set
x is Element of bool ()
y is set
B is epsilon-transitive epsilon-connected ordinal natural set
succ B is non empty epsilon-transitive epsilon-connected ordinal natural set
{B} is non empty set
B \/ {B} is non empty set
r is Element of ()
A is Element of ()
(r,A) is Element of ()
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+
x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
x9 +^ 1 is epsilon-transitive epsilon-connected ordinal natural set
succ x9 is non empty epsilon-transitive epsilon-connected ordinal natural set
{x9} is non empty set
x9 \/ {x9} is non empty set
y9 is epsilon-transitive epsilon-connected ordinal natural set
x is Element of ()
A is Element of ()
B is epsilon-transitive epsilon-connected ordinal natural Element of omega
y is epsilon-transitive epsilon-connected ordinal natural Element of omega
r is epsilon-transitive epsilon-connected ordinal set
B +^ r is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural Element of omega
y9 is Element of RAT+
x9 is Element of RAT+
t1 is Element of RAT+
x9 + t1 is Element of RAT+
numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator x9),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set
numerator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator t1),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator x9),(denominator t1)),K73((numerator t1),(denominator x9))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator x9),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator x9),(denominator t1)),K73((numerator t1),(denominator x9))) / K73((denominator x9),(denominator t1)) is Element of RAT+
B is Element of RAT+
r is Element of RAT+
B + r is Element of RAT+
numerator B is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator r is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator B),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set
numerator r is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator B is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator r),(denominator B)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator B),(denominator r)),K73((numerator r),(denominator B))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator B),(denominator r)) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator B),(denominator r)),K73((numerator r),(denominator B))) / K73((denominator B),(denominator r)) is Element of RAT+
x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
s is epsilon-transitive epsilon-connected ordinal natural Element of omega
x9 +^ s is epsilon-transitive epsilon-connected ordinal natural set
x is Element of ()
y is Element of ()
y9 is Element of ()
(y,y9) is Element of ()
B is Element of ()
(x,B) is Element of ()
(y,B) is Element of ()
(x,(y,B)) is Element of ()
A is Element of ()
(x,A) is Element of ()
x is Element of ()
y is Element of ()
(x,y) is Element of ()
(x) is Element of ()
(y) is Element of ()
((x),(y)) is Element of ()
{ (b₁ *' b₂) where b₁, b₂ is Element of RAT+ : ( b₁ in (x) & b₂ in (y) ) } is set
(((x),(y))) is Element of ()
y9 is Element of RAT+
{} *' y9 is Element of RAT+
numerator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator {}),(numerator y9)) is epsilon-transitive epsilon-connected ordinal natural set
denominator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator {}),(denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator {}),(numerator y9)) / K73((denominator {}),(denominator y9)) is Element of RAT+
y9 is Element of RAT+
y9 *' {} is Element of RAT+
numerator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator y9),(numerator {})) is epsilon-transitive epsilon-connected ordinal natural set
denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator {} is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator y9),(denominator {})) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator y9),(numerator {})) / K73((denominator y9),(denominator {})) is Element of RAT+
y9 is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not y9 <=' b₁ } is set
x9 is Element of RAT+
{ b₁ where b₁ is Element of RAT+ : not x9 <=' b₁ } is set
x9 *' y9 is Element of RAT+
numerator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
numerator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator x9),(numerator y9)) is epsilon-transitive epsilon-connected ordinal natural set
denominator x9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
denominator y9 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator x9),(denominator y9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator x9),(numerator y9)) / K73((denominator x9),(denominator y9)) is Element of RAT+
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 *' t1 is Element of RAT+
K73((numerator x9),(numerator t1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator x9),(denominator t1)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator x9),(numerator t1)) / K73((denominator x9),(denominator t1)) is Element of RAT+
t2 is Element of RAT+
t2 is Element of RAT+
t2 is Element of RAT+
s is Element of RAT+
x9 *' s is Element of RAT+
numerator s is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator x9),(numerator s)) is epsilon-transitive epsilon-connected ordinal natural set
denominator s is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator x9),(denominator s)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator x9),(numerator s)) / K73((denominator x9),(denominator s)) is Element of RAT+
t1 is Element of RAT+
t1 *' x9 is Element of RAT+
numerator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator t1),(numerator x9)) is epsilon-transitive epsilon-connected ordinal natural set
denominator t1 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator t1),(denominator x9)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator t1),(numerator x9)) / K73((denominator t1),(denominator x9)) is Element of RAT+
t2 is Element of RAT+
t1 *' t2 is Element of RAT+
numerator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((numerator t1),(numerator t2)) is epsilon-transitive epsilon-connected ordinal natural set
denominator t2 is epsilon-transitive epsilon-connected ordinal natural Element of omega
K73((denominator t1),(denominator t2)) is epsilon-transitive epsilon-connected ordinal natural set
K73((numerator t1),(numerator t2)) / K73((denominator t1),(denominator t2)) is Element of RAT+
r is Element of RAT+
s is Element of RAT+