:: ARYTM_2 semantic presentation

RAT+ is non empty set

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

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

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

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

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

bool () is non empty set
RA is set
rone is Element of bool RAT+
() is Element of bool ()
{ b1 where b1 is Element of RAT+ : not one <=' b1 } 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
{ { b2 where b2 is Element of RAT+ : not b1 <=' b2 } where b1 is Element of RAT+ : not b1 = {} } is set
(RAT+ \/ ()) \ { { b2 where b2 is Element of RAT+ : not b1 <=' b2 } where b1 is Element of RAT+ : not b1 = {} } 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+
{ b1 where b1 is Element of RAT+ : not x <=' b1 } 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+ \/ { b1 where b1 is Element of bool RAT+ : for b2 being Element of RAT+ holds
( not b2 in b1 or ( ( for b3 being Element of RAT+ holds
( not b3 <=' b2 or b3 in b1 ) ) & ex b3 being Element of RAT+ st
( b3 in b1 & not b3 <=' b2 ) ) )
}
is non empty set

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

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

() \ { { b2 where b2 is Element of RAT+ : not b1 <=' b2 } where b1 is Element of RAT+ : not b1 = {} } is Element of bool ()
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } \ { [b1,1] where b1 is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is Element of bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) }
bool { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } is non empty set
( { [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( b1,b2 are_relative_prime & not b2 = {} ) } \ { [b1,1] where b1 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+
{ b1 where b1 is Element of RAT+ : not x <=' b1 } 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 ()
{ b1 where b1 is Element of RAT+ : not y9 <=' b1 } is set
A is Element of RAT+
y is Element of ()
{ b1 where b1 is Element of RAT+ : not A <=' b1 } 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+
{ b1 where b1 is Element of RAT+ : not x <=' b1 } 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 ()
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 ()
{ b1 where b1 is Element of RAT+ : not {} <=' b1 } is set
x is set
y is Element of RAT+
x is Element of RAT+
{ b1 where b1 is Element of RAT+ : not x <=' b1 } is set
x is Element of RAT+
{ b1 where b1 is Element of RAT+ : not x <=' b1 } 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+
{ b1 where b1 is Element of RAT+ : not y <=' b1 } is set
y9 is set
A is Element of RAT+
y9 is set
A is Element of RAT+
RAT+ /\ () is Element of bool ()
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
{ b1 where b1 is Element of RAT+ : not rone <=' b1 } 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+
{ b1 where b1 is Element of RAT+ : not y <=' b1 } is set
y9 is Element of RAT+
{ b1 where b1 is Element of RAT+ : not y9 <=' b1 } is set
A is Element of RAT+
y is Element of RAT+
{ b1 where b1 is Element of RAT+ : not y <=' b1 } is set
y9 is Element of RAT+
y is Element of RAT+
{ b1 where b1 is Element of RAT+ : not y <=' b1 } 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 ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in rone & b2 in x ) } is set
y9 is set
A is Element of RAT+
B is Element of RAT+
A + B is Element of RAT+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) 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+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) 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+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) is Element of RAT+
y is Element of ()
y9 is Element of ()
A is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in y9 & b2 in A ) } is set
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in A & b2 in y9 ) } is set
r is set
s is Element of RAT+
t1 is Element of RAT+
s + t1 is Element of RAT+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) is Element of RAT+
r is set
s is Element of RAT+
t1 is Element of RAT+
s + t1 is Element of RAT+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) is Element of RAT+
rone is set
x is Element of bool RAT+
rone is Element of ()
x is Element of ()
{ (b1 *' b2) where b1, b2 is Element of RAT+ : ( b1 in rone & b2 in x ) } is set
y is set
y9 is Element of RAT+
A is Element of RAT+
y9 *' A is Element of RAT+

K73((),()) / K73((),()) is Element of RAT+
y9 is set
A is Element of RAT+
B is Element of RAT+
A *' B is Element of RAT+

K73((),()) / K73((),()) 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+

K73((),()) / K73((),()) is Element of RAT+
r is Element of RAT+
s is Element of RAT+
B *' s is Element of RAT+

K73((),()) / K73((),()) is Element of RAT+
r is Element of RAT+
s is Element of RAT+
s *' r is Element of RAT+

K73((),()) / K73((),()) is Element of RAT+
B *' r is Element of RAT+

K73((),()) / K73((),()) is Element of RAT+
A is Element of RAT+
B is Element of RAT+
A *' B is Element of RAT+

K73((),()) / K73((),()) is Element of RAT+
x9 is Element of RAT+
r is Element of RAT+
x9 *' r is Element of RAT+

K73((),()) / K73((),()) is Element of RAT+
y is Element of ()
y9 is Element of ()
A is Element of ()
{ (b1 *' b2) where b1, b2 is Element of RAT+ : ( b1 in y9 & b2 in A ) } is set
{ (b1 *' b2) where b1, b2 is Element of RAT+ : ( b1 in A & b2 in y9 ) } is set
B is set
x9 is Element of RAT+
r is Element of RAT+
x9 *' r is Element of RAT+

K73((),()) / K73((),()) is Element of RAT+
x9 is Element of RAT+
r is Element of RAT+
x9 *' r is Element of RAT+

K73((),()) / K73((),()) is Element of RAT+
s is Element of RAT+
t1 is Element of RAT+
s *' t1 is Element of RAT+

K73((),()) / K73((),()) is Element of RAT+
x9 is Element of RAT+
r is Element of RAT+
x9 *' r is Element of RAT+

K73((),()) / K73((),()) 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 ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (rone) & b2 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 ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (y9) & b2 in (A) ) } is set
(((y9),(A))) is Element of ()
((A),(y9)) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (A) & b2 in (y9) ) } is set
(((A),(y9))) is Element of ()
((rone),(x)) is Element of ()
{ (b1 *' b2) where b1, b2 is Element of RAT+ : ( b1 in (rone) & b2 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 ()
{ (b1 *' b2) where b1, b2 is Element of RAT+ : ( b1 in (y9) & b2 in (A) ) } is set
(((y9),(A))) is Element of ()
((A),(y9)) is Element of ()
{ (b1 *' b2) where b1, b2 is Element of RAT+ : ( b1 in (A) & b2 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 ()
{ (b1 *' b2) where b1, b2 is Element of RAT+ : ( b1 in (rone) & b2 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+

K73((),()) / K73((),()) 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+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) is Element of RAT+
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (rone) & b2 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 ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in x & b2 in y ) } is set
(rone,(x,y)) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in rone & b2 in (x,y) ) } is set
(rone,x) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in rone & b2 in x ) } is set
((rone,x),y) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (rone,x) & b2 in y ) } is set
y9 is set
A is Element of RAT+
B is Element of RAT+
A + B is Element of RAT+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

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

K73((),(denominator (A + x9))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (A + x9)),()),K73((),(denominator (A + x9)))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator (A + x9)),()) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (A + x9)),()),K73((),(denominator (A + x9)))) / K73((denominator (A + x9)),()) is Element of RAT+
rone is Element of ()
x is Element of ()
y is Element of ()
(x,y) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in x & b2 in y ) } is set
(rone,(x,y)) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in rone & b2 in (x,y) ) } is set
(rone,x) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in rone & b2 in x ) } is set
((rone,x),y) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (rone,x) & b2 in y ) } is set
rone is Element of ()
x is Element of ()
(rone,x) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in rone & b2 in x ) } is set
y is Element of RAT+
y9 is Element of RAT+
y + y9 is Element of RAT+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) 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 ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (x) & b2 in (y) ) } is set
(((x),(y))) is Element of ()
(rone) is Element of ()
((rone),(x)) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (rone) & b2 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 ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (rone) & b2 in ((((x),(y)))) ) } is set
(((rone),((((x),(y)))))) is Element of ()
((rone),((x),(y))) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (rone) & b2 in ((x),(y)) ) } is set
(((rone),((x),(y)))) is Element of ()
(((rone),(x)),(y)) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in ((rone),(x)) & b2 in (y) ) } is set
((((rone),(x)),(y))) is Element of ()
((((rone),(x)))) is Element of ()
(((((rone),(x)))),(y)) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in ((((rone),(x)))) & b2 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+
{ b1 where b1 is Element of RAT+ : not y <=' b1 } 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 ()
{ b1 where b1 is Element of RAT+ : ex b2, b3 being Element of () st
( b3 = b1 & b2 in rone & (b2,b3) )
}
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+
{ b1 where b1 is Element of RAT+ : not A <=' b1 } 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 ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in rone & b2 in x ) } is set
y is Element of RAT+
{} *' y is Element of RAT+

K73((),()) / K73(,()) 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+

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

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

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

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

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

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

K73((numerator ()),(denominator (B *' y))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (B *' y)),(denominator ())),K73((numerator ()),(denominator (B *' y)))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator (B *' y)),(denominator ())) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (B *' y)),(denominator ())),K73((numerator ()),(denominator (B *' y)))) / K73((denominator (B *' y)),(denominator ())) is Element of RAT+
(B *' y) + y is Element of RAT+

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

K72(K73((numerator (B *' y)),()),K73((),(denominator (B *' y)))) / K73((denominator (B *' 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 ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (rone) & b2 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+
{ b1 where b1 is Element of RAT+ : ex b2, b3 being Element of RAT+ st
( not b2 in rone & b3 in x & b2 + b1 = b3 )
}
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+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),),K73((),())) / K73((),) 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+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

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

K73((),(denominator (x9 + s))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (x9 + s)),()),K73((),(denominator (x9 + s)))) is epsilon-transitive epsilon-connected ordinal natural set
K73((denominator (x9 + s)),()) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((numerator (x9 + s)),()),K73((),(denominator (x9 + s)))) / K73((denominator (x9 + s)),()) is Element of RAT+
t2 + t1 is Element of RAT+
K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

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

K73((numerator (B + t1)),()) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((),(denominator (B + t1))),K73((numerator (B + t1)),())) is epsilon-transitive epsilon-connected ordinal natural set
K73((),(denominator (B + t1))) is epsilon-transitive epsilon-connected ordinal natural set
K72(K73((),(denominator (B + t1))),K73((numerator (B + t1)),())) / K73((),(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+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) is Element of RAT+
x9 is Element of ()
(rone,x9) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in rone & b2 in x9 ) } is set
s is set
t1 is Element of RAT+
t1 + {} is Element of RAT+

K72(K73((),),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),),K73((),())) / K73((),) is Element of RAT+
t1 is Element of RAT+
t2 is Element of RAT+
{ b1 where b1 is Element of RAT+ : ex b2 being Element of RAT+ st
( not b2 in rone & b2 + b1 = t2 )
}
is set

t2 + {} is Element of RAT+

K72(K73((),),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) is Element of RAT+
{} *' rr is Element of RAT+

K73((),()) / K73(,()) is Element of RAT+
n0 is Element of RAT+
n0 *' rr is Element of RAT+

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

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

K72(K73((),),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

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

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

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

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

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

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

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

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

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+

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

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) 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+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) 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+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

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

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) 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 ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (rone) & b2 in y ) } is set
(y) is Element of ()
(rone,(y)) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in y & b2 in (rone) ) } is set
y9 is set
A is Element of RAT+
B is Element of RAT+
A + B is Element of RAT+

K72(K73((),()),K73((),())) is epsilon-transitive epsilon-connected ordinal natural set

K72(K73((),()),K73((),())) / K73((),()) is Element of RAT+
((y)) is Element of ()
((rone),((y))) is Element of ()
{ (b1 + b2) where b1, b2 is Element of RAT+ : ( b1 in (rone) & b2 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 ()
{ (b1 *' b2) where b1, b2 is Element of RAT+ : ( b1 in x & b2 in y ) } is set
(rone,(x,y)) is Element of ()
{ (b1 *' b2) where b1, b2 is Element of RAT+ : ( b1 in rone & b2 in (x,y) ) } is set
(rone,x) is Element of ()
{ (b1 *' b2) where b1, b2 is Element of RAT+ : ( b1 in rone & b2 in x ) } is set
((rone,x),y) is Element of ()
{ (b1 *' b2) where b1, b2 is Element of RAT+ : ( b1 in (rone,x) & b2 in y ) } is set
y9 is set
A is Element of RAT+
B is Element of RAT+
A *' B is Element of RAT+