:: ARYTM_3 semantic presentation

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

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

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

() is set

A is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

c

s *^ c

c

s *^ c

{} *^ {} is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal set

RATplus is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

RATplus *^ A is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

RATplus *^ B is epsilon-transitive epsilon-connected ordinal set

RATplus is epsilon-transitive epsilon-connected ordinal set

RATplus *^ {} is epsilon-transitive epsilon-connected ordinal set

RATplus *^ 1 is epsilon-transitive epsilon-connected ordinal set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal natural set

c

c

s is epsilon-transitive epsilon-connected ordinal natural set

s *^ c

s *^ c

A is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal natural set

c

c

s is epsilon-transitive epsilon-connected ordinal natural set

s *^ c

s *^ c

A is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

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

1 *^ s is epsilon-transitive epsilon-connected ordinal natural set

c

1 *^ c

c

r is epsilon-transitive epsilon-connected ordinal set

c

x is epsilon-transitive epsilon-connected ordinal set

c

s1 is epsilon-transitive epsilon-connected ordinal natural Element of omega

s2 is epsilon-transitive epsilon-connected ordinal natural Element of omega

1 *^ s2 is epsilon-transitive epsilon-connected ordinal natural set

d19 is epsilon-transitive epsilon-connected ordinal natural set

d29 is epsilon-transitive epsilon-connected ordinal natural set

c9 is epsilon-transitive epsilon-connected ordinal natural set

c9 *^ d19 is epsilon-transitive epsilon-connected ordinal natural set

dx is epsilon-transitive epsilon-connected ordinal natural Element of omega

c9 *^ d29 is epsilon-transitive epsilon-connected ordinal natural set

s1 *^ c9 is epsilon-transitive epsilon-connected ordinal natural set

(s1 *^ c9) *^ d19 is epsilon-transitive epsilon-connected ordinal natural set

(s1 *^ c9) *^ d29 is epsilon-transitive epsilon-connected ordinal natural set

s2 *^ s1 is epsilon-transitive epsilon-connected ordinal natural set

dx *^ s1 is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ RATplus is epsilon-transitive epsilon-connected ordinal set

{} *^ 1 is epsilon-transitive epsilon-connected ordinal natural set

(RATplus div^ RATplus) *^ 1 is epsilon-transitive epsilon-connected ordinal set

(RATplus div^ RATplus) *^ RATplus is epsilon-transitive epsilon-connected ordinal set

RATplus mod^ RATplus is epsilon-transitive epsilon-connected ordinal set

(RATplus div^ RATplus) *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

((RATplus div^ RATplus) *^ RATplus) +^ (RATplus mod^ RATplus) is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

A *^ 1 is epsilon-transitive epsilon-connected ordinal set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal set

RATplus *^ A is epsilon-transitive epsilon-connected ordinal set

RATplus *^ {} is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ A is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus mod^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus div^ RATplus) *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus -^ ((RATplus div^ RATplus) *^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal set

((RATplus div^ RATplus) *^ RATplus) +^ A is epsilon-transitive epsilon-connected ordinal set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ (RATplus div^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ A is epsilon-transitive epsilon-connected ordinal natural set

{} *^ A is epsilon-transitive epsilon-connected ordinal natural set

A *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

(A *^ RATplus) +^ {} is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ (RATplus div^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus div^ RATplus) *^ (RATplus div^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ (RATplus div^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ 1 is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ ((RATplus div^ RATplus) *^ (RATplus div^ RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ {} is epsilon-transitive epsilon-connected ordinal natural set

1 *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal set

RATplus *^ A is epsilon-transitive epsilon-connected ordinal set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal natural set

RATplus +^ A is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ B is epsilon-transitive epsilon-connected ordinal natural set

s is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ s is epsilon-transitive epsilon-connected ordinal natural set

(RATplus *^ s) -^ (RATplus *^ B) is epsilon-transitive epsilon-connected ordinal natural set

s -^ B is epsilon-transitive epsilon-connected ordinal natural set

(s -^ B) *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

succ {} is non empty epsilon-transitive epsilon-connected ordinal natural set

{{}} is non empty set

{} \/ {{}} is non empty set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

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

B is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ 1 is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal natural set

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

c

c

s *^ (c

c

(s *^ (c

s div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ (s div^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(s div^ RATplus) *^ (c

RATplus *^ ((s div^ RATplus) *^ (c

s div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ (s div^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(s div^ RATplus) *^ (c

RATplus *^ ((s div^ RATplus) *^ (c

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

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

B is epsilon-transitive epsilon-connected ordinal natural set

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

s is epsilon-transitive epsilon-connected ordinal natural set

c

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus *^ RATplus) div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

((RATplus *^ RATplus) div^ (RATplus,RATplus)) *^ ((RATplus,RATplus) div^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ ((RATplus,RATplus) div^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) *^ ((RATplus *^ RATplus) div^ (RATplus,RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

((RATplus,RATplus) div^ RATplus) *^ ((RATplus *^ RATplus) div^ (RATplus,RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ (((RATplus,RATplus) div^ RATplus) *^ ((RATplus *^ RATplus) div^ (RATplus,RATplus))) is epsilon-transitive epsilon-connected ordinal natural set

((RATplus *^ RATplus) div^ (RATplus,RATplus)) *^ ((RATplus,RATplus) div^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus \/ RATplus is epsilon-transitive epsilon-connected ordinal set

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

B is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus *^ RATplus) div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

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

B is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ B is epsilon-transitive epsilon-connected ordinal natural set

B *^ (RATplus div^ B) is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ B is epsilon-transitive epsilon-connected ordinal natural set

B *^ (RATplus div^ B) is epsilon-transitive epsilon-connected ordinal natural set

(B *^ (RATplus div^ B)) *^ (RATplus div^ B) is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ (RATplus div^ B) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus div^ B) *^ (RATplus div^ B) is epsilon-transitive epsilon-connected ordinal natural set

B *^ ((RATplus div^ B) *^ (RATplus div^ B)) is epsilon-transitive epsilon-connected ordinal natural set

(B *^ ((RATplus div^ B) *^ (RATplus div^ B))) div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) *^ ((B *^ ((RATplus div^ B) *^ (RATplus div^ B))) div^ (RATplus,RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus *^ RATplus) +^ {} is epsilon-transitive epsilon-connected ordinal natural set

(B *^ ((RATplus div^ B) *^ (RATplus div^ B))) *^ B is epsilon-transitive epsilon-connected ordinal natural set

B *^ ((B *^ ((RATplus div^ B) *^ (RATplus div^ B))) div^ (RATplus,RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) *^ (B *^ ((B *^ ((RATplus div^ B) *^ (RATplus div^ B))) div^ (RATplus,RATplus))) is epsilon-transitive epsilon-connected ordinal natural set

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

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

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

B is epsilon-transitive epsilon-connected ordinal natural set

s is epsilon-transitive epsilon-connected ordinal natural set

c

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,{}) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,{}) is epsilon-transitive epsilon-connected ordinal natural Element of omega

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

B is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural Element of omega

B is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) *^ (RATplus div^ (RATplus,RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus is epsilon-transitive epsilon-connected ordinal natural Element of omega

A is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal natural set

A *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

((RATplus *^ RATplus),(A *^ RATplus)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,A) *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

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

((RATplus *^ RATplus),(A *^ RATplus)) div^ B is epsilon-transitive epsilon-connected ordinal natural set

A div^ (RATplus,A) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,A) *^ (A div^ (RATplus,A)) is epsilon-transitive epsilon-connected ordinal natural set

B *^ (A div^ (RATplus,A)) is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ (RATplus,A) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,A) *^ (RATplus div^ (RATplus,A)) is epsilon-transitive epsilon-connected ordinal natural set

B *^ (RATplus div^ (RATplus,A)) is epsilon-transitive epsilon-connected ordinal natural set

B *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B) is epsilon-transitive epsilon-connected ordinal natural set

((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

(A *^ RATplus) div^ (((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ RATplus) *^ ((A *^ RATplus) div^ (((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ ((A *^ RATplus) div^ (((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

(((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ ((A *^ RATplus) div^ (((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ RATplus))) *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus *^ RATplus) div^ (((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ RATplus) *^ ((RATplus *^ RATplus) div^ (((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ ((RATplus *^ RATplus) div^ (((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

(((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ ((RATplus *^ RATplus) div^ (((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ RATplus))) *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,A) div^ ((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) is epsilon-transitive epsilon-connected ordinal natural set

((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)) *^ ((RATplus,A) div^ ((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B))) is epsilon-transitive epsilon-connected ordinal natural set

(((RATplus *^ RATplus),(A *^ RATplus)) div^ B) *^ ((RATplus,A) div^ ((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B))) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,A) *^ ((((RATplus *^ RATplus),(A *^ RATplus)) div^ B) *^ ((RATplus,A) div^ ((RATplus,A) *^ (((RATplus *^ RATplus),(A *^ RATplus)) div^ B)))) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,A) *^ 1 is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) *^ (RATplus div^ (RATplus,RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

1 *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

1 *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) *^ (RATplus div^ (RATplus,RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

B *^ s is epsilon-transitive epsilon-connected ordinal set

c

B *^ c

(RATplus,RATplus) *^ (RATplus div^ (RATplus,RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

c

(RATplus,RATplus) *^ c

x is epsilon-transitive epsilon-connected ordinal natural Element of omega

((RATplus,RATplus) *^ c

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

((RATplus,RATplus) *^ c

(RATplus,RATplus) div^ ((RATplus,RATplus) *^ c

((RATplus,RATplus) *^ c

c

(RATplus,RATplus) *^ (c

(RATplus,RATplus) *^ 1 is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) *^ (RATplus div^ (RATplus,RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) *^ (RATplus div^ (RATplus,RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

A *^ B is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

A *^ s is epsilon-transitive epsilon-connected ordinal set

c

c

c

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) *^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,1) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,1) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,1) is epsilon-transitive epsilon-connected ordinal natural set

(1,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(1,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

1 div^ (1,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

({},RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

({},RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

{} div^ ({},RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,{}) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,{}) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,{}) is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ 1 is epsilon-transitive epsilon-connected ordinal natural set

(RATplus *^ 1) div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,RATplus) is epsilon-transitive epsilon-connected ordinal natural set

RATplus div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ 1 is epsilon-transitive epsilon-connected ordinal natural set

(RATplus *^ 1) div^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus is epsilon-transitive epsilon-connected ordinal natural set

RATplus *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal natural set

A *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

((RATplus *^ RATplus),(A *^ RATplus)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((RATplus *^ RATplus),(A *^ RATplus)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus *^ RATplus) div^ ((RATplus *^ RATplus),(A *^ RATplus)) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(RATplus,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

RATplus div^ (RATplus,A) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,A) *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

({},A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

({},A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

{} div^ ({},A) is epsilon-transitive epsilon-connected ordinal natural set

{} *^ ((RATplus,A) *^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus *^ RATplus) div^ ((RATplus,A) *^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus div^ (RATplus,A)) *^ (RATplus,A) is epsilon-transitive epsilon-connected ordinal natural set

((RATplus div^ (RATplus,A)) *^ (RATplus,A)) *^ RATplus is epsilon-transitive epsilon-connected ordinal natural set

(((RATplus div^ (RATplus,A)) *^ (RATplus,A)) *^ RATplus) div^ ((RATplus,A) *^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

(RATplus,A) *^ ((RATplus,A) *^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

((RATplus,A) *^ ((RATplus,A) *^ RATplus)) div^ ((RATplus,A) *^ RATplus) is epsilon-transitive epsilon-connected ordinal natural set

{ [b

[1,1] is set

{1,1} is non empty set

{1} is non empty set

{{1,1},{1}} is non empty set

RATplus is non empty set

A is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal natural set

[A,B] is set

{A,B} is non empty set

{A} is non empty set

{{A,B},{A}} is non empty set

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

c

[s,c

{s,c

{s} is non empty set

{{s,c

{ [b

{ [b

K6( { [b

( { [b

() is set

A is Element of ()

RATplus \ { [b

K6(RATplus) is non empty set

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

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

[B,s] is set

{B,s} is non empty set

{B} is non empty set

{{B,s},{B}} is non empty set

[B,1] is set

{B,1} is non empty set

{{B,1},{B}} is non empty set

A is set

B is set

[A,B] is set

{A,B} is non empty set

{A} is non empty set

{{A,B},{A}} is non empty set

A is epsilon-transitive epsilon-connected ordinal set

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

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

[B,s] is set

{B,s} is non empty set

{B} is non empty set

{{B,s},{B}} is non empty set

A is epsilon-transitive epsilon-connected ordinal Element of ()

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

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

[B,s] is set

{B,s} is non empty set

{B} is non empty set

{{B,s},{B}} is non empty set

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

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

[B,s] is set

{B,s} is non empty set

{B} is non empty set

{{B,s},{B}} is non empty set

A is set

B is set

[A,B] is set

{A,B} is non empty set

{A} is non empty set

{{A,B},{A}} is non empty set

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

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

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

[A,B] is set

{A,B} is non empty set

{A} is non empty set

{{A,B},{A}} is non empty set

RATplus \ { [b

K6(RATplus) is non empty set

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

[s,1] is set

{s,1} is non empty set

{s} is non empty set

{{s,1},{s}} is non empty set

A is Element of ()

RATplus \ { [b

K6(RATplus) is non empty set

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

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

[B,s] is set

{B,s} is non empty set

{B} is non empty set

{{B,s},{B}} is non empty set

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

c

c

x is epsilon-transitive epsilon-connected ordinal natural set

[c

{c

{c

{{c

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

s1 is epsilon-transitive epsilon-connected ordinal natural set

[r,s1] is set

{r,s1} is non empty set

{r} is non empty set

{{r,s1},{r}} is non empty set

RATplus \ { [b

K6(RATplus) is non empty set

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

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

[B,s] is set

{B,s} is non empty set

{B} is non empty set

{{B,s},{B}} is non empty set

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

c

x is epsilon-transitive epsilon-connected ordinal natural set

c

[x,c

{x,c

{x} is non empty set

{{x,c

s1 is epsilon-transitive epsilon-connected ordinal natural set

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

[s1,r] is set

{s1,r} is non empty set

{s1} is non empty set

{{s1,r},{s1}} is non empty set

A is Element of ()

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

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

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

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

[B,s] is set

{B,s} is non empty set

{B} is non empty set

{{B,s},{B}} is non empty set

A is Element of ()

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

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

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

[B,s] is set

{B,s} is non empty set

{B} is non empty set

{{B,s},{B}} is non empty set

A is Element of ()

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

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

[(A),(A)] is set

{(A),(A)} is non empty set

{(A)} is non empty set

{{(A),(A)},{(A)}} is non empty set

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

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

[B,s] is set

{B,s} is non empty set

{B} is non empty set

{{B,s},{B}} is non empty set

A is Element of ()

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

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

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

[B,s] is set

{B,s} is non empty set

{B} is non empty set

{{B,s},{B}} is non empty set

A is Element of ()

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

B is Element of ()

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

B is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal natural set

(B,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(B,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

B div^ (B,A) is epsilon-transitive epsilon-connected ordinal natural set

(A,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

A div^ (A,B) is epsilon-transitive epsilon-connected ordinal natural set

[(A,B),(B,A)] is set

{(A,B),(B,A)} is non empty set

{(A,B)} is non empty set

{{(A,B),(B,A)},{(A,B)}} is non empty set

s is Element of ()

A is Element of ()

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

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

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

((A),(A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((A),(A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A) div^ ((A),(A)) is epsilon-transitive epsilon-connected ordinal natural set

((A),(A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((A),(A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A) div^ ((A),(A)) is epsilon-transitive epsilon-connected ordinal natural set

[(A),(A)] is set

{(A),(A)} is non empty set

{(A)} is non empty set

{{(A),(A)},{(A)}} is non empty set

A is epsilon-transitive epsilon-connected ordinal natural set

({},A) is Element of ()

B is epsilon-transitive epsilon-connected ordinal natural set

(B,1) is Element of ()

(A,{}) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A,{}) is epsilon-transitive epsilon-connected ordinal natural Element of omega

A div^ (A,{}) is epsilon-transitive epsilon-connected ordinal natural set

({},A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

({},A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

{} div^ ({},A) is epsilon-transitive epsilon-connected ordinal natural set

(1,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(1,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

1 div^ (1,B) is epsilon-transitive epsilon-connected ordinal natural set

(B,1) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(B,1) is epsilon-transitive epsilon-connected ordinal natural Element of omega

B div^ (B,1) is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal natural set

(A,A) is Element of ()

(A,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

A div^ (A,A) is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal natural set

(B,A) is Element of ()

((B,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(B,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(B,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

B div^ (B,A) is epsilon-transitive epsilon-connected ordinal natural set

((B,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

A div^ (A,B) is epsilon-transitive epsilon-connected ordinal natural set

[(B,A),(A,B)] is set

{(B,A),(A,B)} is non empty set

{(B,A)} is non empty set

{{(B,A),(A,B)},{(B,A)}} is non empty set

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

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

(A,B) is Element of ()

((A,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((A,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

A div^ (A,B) is epsilon-transitive epsilon-connected ordinal natural set

(B,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(B,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega

B div^ (B,A) is epsilon-transitive epsilon-connected ordinal natural set

A is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal natural set

B *^ A is epsilon-transitive epsilon-connected ordinal natural set

s is epsilon-transitive epsilon-connected ordinal natural set

s *^ A is epsilon-transitive epsilon-connected ordinal natural set

((B *^ A),(s *^ A)) is Element of ()

(B,s) is Element of ()

(((B *^ A),(s *^ A))) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((s *^ A),(B *^ A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((s *^ A),(B *^ A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(s *^ A) div^ ((s *^ A),(B *^ A)) is epsilon-transitive epsilon-connected ordinal natural set

(s,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(s,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

s div^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set

((B,s)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(((B *^ A),(s *^ A))) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((B *^ A),(s *^ A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((B *^ A),(s *^ A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(B *^ A) div^ ((B *^ A),(s *^ A)) is epsilon-transitive epsilon-connected ordinal natural set

(B,s) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(B,s) is epsilon-transitive epsilon-connected ordinal natural Element of omega

B div^ (B,s) is epsilon-transitive epsilon-connected ordinal natural set

((B,s)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(((B,s)),((B,s))) is Element of ()

A is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal natural set

s is epsilon-transitive epsilon-connected ordinal natural set

(s,B) is Element of ()

s *^ A is epsilon-transitive epsilon-connected ordinal natural set

c

(c

B *^ c

((c

((c

(c

(c

c

((s,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((s,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(B,s) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(B,s) is epsilon-transitive epsilon-connected ordinal natural Element of omega

B div^ (B,s) is epsilon-transitive epsilon-connected ordinal natural set

(A,c

(A,c

A div^ (A,c

(s,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(s,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

s div^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set

((c

((s,B)) *^ (A,c

(((c

((((c

(s,B) *^ ((s,B)) is epsilon-transitive epsilon-connected ordinal natural set

((c

(((c

((c

(((c

((c

B *^ (((c

B *^ A is epsilon-transitive epsilon-connected ordinal natural set

((B *^ A),(B *^ c

((B *^ A),(B *^ c

(B *^ A) div^ ((B *^ A),(B *^ c

((B *^ c

((B *^ c

(B *^ c

(((c

A is Element of ()

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

B is Element of ()

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

(A) *^ (B) is epsilon-transitive epsilon-connected ordinal natural set

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

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

(B) *^ (A) is epsilon-transitive epsilon-connected ordinal natural set

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

(A) *^ (B) is epsilon-transitive epsilon-connected ordinal natural set

((((A) *^ (B)) +^ ((B) *^ (A))),((A) *^ (B))) is Element of ()

s is Element of ()

c

(c

c

(c

(c

(c

(c

(c

((c

(c

((((c

((c

(c

((((c

(A) *^ (B) is epsilon-transitive epsilon-connected ordinal natural set

(((A) *^ (B)),((A) *^ (B))) is Element of ()

s is Element of ()

c

(c

c

(c

(c

(c

(c

(c

(((c

(c

(c

(((c

A is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal natural set

B *^ A is epsilon-transitive epsilon-connected ordinal natural set

s is epsilon-transitive epsilon-connected ordinal natural set

(s,B) is Element of ()

s *^ A is epsilon-transitive epsilon-connected ordinal natural set

c

(c

((s,B),(c

((s,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((c

((s,B)) *^ ((c

((c

((s,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((c

(((s,B)) *^ ((c

((s,B)) *^ ((c

(((((s,B)) *^ ((c

B *^ c

(s *^ A) +^ (B *^ c

(((s *^ A) +^ (B *^ c

(A,c

(A,c

A div^ (A,c

(B,s) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(B,s) is epsilon-transitive epsilon-connected ordinal natural Element of omega

B div^ (B,s) is epsilon-transitive epsilon-connected ordinal natural set

(c

(c

c

(s,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(s,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

s div^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set

(s,B) *^ (A,c

(B,s) *^ (c

((s,B) *^ (A,c

(((s,B) *^ (A,c

(B,s) *^ (A,c

((B,s) *^ (A,c

(((((s,B) *^ (A,c

(B,s) *^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set

(A,c

(((((s,B) *^ (A,c

(A,c

(((((s,B) *^ (A,c

((s,B) *^ (A,c

((B,s) *^ (c

(((s,B) *^ (A,c

(((((s,B) *^ (A,c

(s,B) *^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set

(A,c

((A,c

((((A,c

(A,c

((A,c

((((A,c

(c

((A,c

((((A,c

(c

((A,c

((((A,c

(((A,c

((A,c

(((((A,c

(A,c

B *^ ((A,c

(((((A,c

(((((A,c

((A,c

((c

(((A,c

(((((A,c

s *^ ((A,c

(s *^ ((A,c

(((s *^ ((A,c

(s *^ A) +^ (((c

(((s *^ A) +^ (((c

(c

B *^ ((c

(s *^ A) +^ (B *^ ((c

(((s *^ A) +^ (B *^ ((c

A is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal natural set

(B,A) is Element of ()

s is epsilon-transitive epsilon-connected ordinal natural set

(s,A) is Element of ()

((B,A),(s,A)) is Element of ()

((B,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((s,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((B,A)) *^ ((s,A)) is epsilon-transitive epsilon-connected ordinal natural set

((s,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((B,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((s,A)) *^ ((B,A)) is epsilon-transitive epsilon-connected ordinal natural set

(((B,A)) *^ ((s,A))) +^ (((s,A)) *^ ((B,A))) is epsilon-transitive epsilon-connected ordinal natural set

((B,A)) *^ ((s,A)) is epsilon-transitive epsilon-connected ordinal natural set

(((((B,A)) *^ ((s,A))) +^ (((s,A)) *^ ((B,A)))),(((B,A)) *^ ((s,A)))) is Element of ()

B +^ s is epsilon-transitive epsilon-connected ordinal natural set

((B +^ s),A) is Element of ()

B *^ A is epsilon-transitive epsilon-connected ordinal natural set

s *^ A is epsilon-transitive epsilon-connected ordinal natural set

(B *^ A) +^ (s *^ A) is epsilon-transitive epsilon-connected ordinal natural set

A *^ A is epsilon-transitive epsilon-connected ordinal natural set

(((B *^ A) +^ (s *^ A)),(A *^ A)) is Element of ()

(B +^ s) *^ A is epsilon-transitive epsilon-connected ordinal natural set

(((B +^ s) *^ A),(A *^ A)) is Element of ()

() is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Element of ()

A is Element of ()

(A,()) is Element of ()

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

(()) is epsilon-transitive epsilon-connected ordinal natural Element of omega

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

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

(()) is epsilon-transitive epsilon-connected ordinal natural Element of omega

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

(((A) *^ (())),((A) *^ (()))) is Element of ()

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

A is epsilon-transitive epsilon-connected ordinal natural set

B is epsilon-transitive epsilon-connected ordinal natural set

s is epsilon-transitive epsilon-connected ordinal natural set

(B,s) is Element of ()

s *^ A is epsilon-transitive epsilon-connected ordinal natural set

c

(c

((B,s),(c

((B,s)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((c

((B,s)) *^ ((c

((B,s)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((c

((B,s)) *^ ((c

((((B,s)) *^ ((c

B *^ c

((B *^ c

(A,c

(A,c

A div^ (A,c

(s,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(s,B) is epsilon-transitive epsilon-connected ordinal natural Element of omega

s div^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set

(c

(c

c

(B,s) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(B,s) is epsilon-transitive epsilon-connected ordinal natural Element of omega

B div^ (B,s) is epsilon-transitive epsilon-connected ordinal natural set

(B,s) *^ (c

((B,s) *^ (c

(s,B) *^ (A,c

((s,B) *^ (A,c

((((B,s) *^ (c

(B,s) *^ (B,s) is epsilon-transitive epsilon-connected ordinal natural set

(c

(((c

(c

(((c

(s,B) *^ (B,s) is epsilon-transitive epsilon-connected ordinal natural set

(A,c

(((c

(A,c

(((c

((c

((A,c

((((c

(c

B *^ ((c

((B *^ ((c

((B *^ c

(A,c

s *^ ((A,c

((B *^ c

A is Element of ()

(A,()) is Element of ()

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

(()) is epsilon-transitive epsilon-connected ordinal natural Element of omega

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

(()) is epsilon-transitive epsilon-connected ordinal natural Element of omega

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

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

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

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

((((A) *^ (())) +^ ((()) *^ (A))),((A) *^ (()))) is Element of ()

(A) *^ 1 is epsilon-transitive epsilon-connected ordinal natural set

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

(A) *^ 1 is epsilon-transitive epsilon-connected ordinal natural set

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

A is Element of ()

B is Element of ()

(A,B) is Element of ()

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

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

(A) *^ (B) is epsilon-transitive epsilon-connected ordinal natural set

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

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

(B) *^ (A) is epsilon-transitive epsilon-connected ordinal natural set

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

(A) *^ (B) is epsilon-transitive epsilon-connected ordinal natural set

((((A) *^ (B)) +^ ((B) *^ (A))),((A) *^ (B))) is Element of ()

s is Element of ()

((A,B),s) is Element of ()

((A,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

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

((A,B)) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

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

((A,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(s) *^ ((A,B)) is epsilon-transitive epsilon-connected ordinal natural set

(((A,B)) *^ (s)) +^ ((s) *^ ((A,B))) is epsilon-transitive epsilon-connected ordinal natural set

((A,B)) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

(((((A,B)) *^ (s)) +^ ((s) *^ ((A,B)))),(((A,B)) *^ (s))) is Element of ()

(B,s) is Element of ()

(B) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

(s) *^ (B) is epsilon-transitive epsilon-connected ordinal natural set

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

(B) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

((((B) *^ (s)) +^ ((s) *^ (B))),((B) *^ (s))) is Element of ()

(A,(B,s)) is Element of ()

((B,s)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A) *^ ((B,s)) is epsilon-transitive epsilon-connected ordinal natural set

((B,s)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

((B,s)) *^ (A) is epsilon-transitive epsilon-connected ordinal natural set

((A) *^ ((B,s))) +^ (((B,s)) *^ (A)) is epsilon-transitive epsilon-connected ordinal natural set

(A) *^ ((B,s)) is epsilon-transitive epsilon-connected ordinal natural set

((((A) *^ ((B,s))) +^ (((B,s)) *^ (A))),((A) *^ ((B,s)))) is Element of ()

(A) *^ (B) is epsilon-transitive epsilon-connected ordinal natural set

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

((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B))) is Element of ()

((s),(s)) is Element of ()

(((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B))),((s),(s))) is Element of ()

(((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B)))) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(((s),(s))) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B)))) *^ (((s),(s))) is epsilon-transitive epsilon-connected ordinal natural set

(((s),(s))) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B)))) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(((s),(s))) *^ (((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B)))) is epsilon-transitive epsilon-connected ordinal natural set

((((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B)))) *^ (((s),(s)))) +^ ((((s),(s))) *^ (((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B))))) is epsilon-transitive epsilon-connected ordinal natural set

(((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B)))) *^ (((s),(s))) is epsilon-transitive epsilon-connected ordinal natural set

((((((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B)))) *^ (((s),(s)))) +^ ((((s),(s))) *^ (((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B)))))),((((((A) *^ (B)) +^ ((A) *^ (B))),((A) *^ (B)))) *^ (((s),(s))))) is Element of ()

(((A) *^ (B)) +^ ((A) *^ (B))) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

((A) *^ (B)) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

((((A) *^ (B)) +^ ((A) *^ (B))) *^ (s)) +^ (((A) *^ (B)) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

((A) *^ (B)) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

((((((A) *^ (B)) +^ ((A) *^ (B))) *^ (s)) +^ (((A) *^ (B)) *^ (s))),(((A) *^ (B)) *^ (s))) is Element of ()

((A) *^ (B)) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

((A) *^ (B)) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

(((A) *^ (B)) *^ (s)) +^ (((A) *^ (B)) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

((((A) *^ (B)) *^ (s)) +^ (((A) *^ (B)) *^ (s))) +^ (((A) *^ (B)) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

((((((A) *^ (B)) *^ (s)) +^ (((A) *^ (B)) *^ (s))) +^ (((A) *^ (B)) *^ (s))),(((A) *^ (B)) *^ (s))) is Element of ()

(A) *^ ((B) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

((A) *^ ((B) *^ (s))) +^ (((A) *^ (B)) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

(((A) *^ ((B) *^ (s))) +^ (((A) *^ (B)) *^ (s))) +^ (((A) *^ (B)) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

(((((A) *^ ((B) *^ (s))) +^ (((A) *^ (B)) *^ (s))) +^ (((A) *^ (B)) *^ (s))),(((A) *^ (B)) *^ (s))) is Element of ()

(A) *^ ((B) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

((A) *^ ((B) *^ (s))) +^ ((A) *^ ((B) *^ (s))) is epsilon-transitive epsilon-connected ordinal natural set

(((A) *^ ((B) *^ (s))) +^ ((A) *^ ((B) *^ (s)))) +^ (((A) *^ (B)) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

(((((A) *^ ((B) *^ (s))) +^ ((A) *^ ((B) *^ (s)))) +^ (((A) *^ (B)) *^ (s))),(((A) *^ (B)) *^ (s))) is Element of ()

(B) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

(A) *^ ((B) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

(((A) *^ ((B) *^ (s))) +^ ((A) *^ ((B) *^ (s)))) +^ ((A) *^ ((B) *^ (s))) is epsilon-transitive epsilon-connected ordinal natural set

(((((A) *^ ((B) *^ (s))) +^ ((A) *^ ((B) *^ (s)))) +^ ((A) *^ ((B) *^ (s)))),(((A) *^ (B)) *^ (s))) is Element of ()

((A) *^ ((B) *^ (s))) +^ ((A) *^ ((B) *^ (s))) is epsilon-transitive epsilon-connected ordinal natural set

((A) *^ ((B) *^ (s))) +^ (((A) *^ ((B) *^ (s))) +^ ((A) *^ ((B) *^ (s)))) is epsilon-transitive epsilon-connected ordinal natural set

((((A) *^ ((B) *^ (s))) +^ (((A) *^ ((B) *^ (s))) +^ ((A) *^ ((B) *^ (s))))),(((A) *^ (B)) *^ (s))) is Element of ()

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

(A) *^ (((B) *^ (s)) +^ ((B) *^ (s))) is epsilon-transitive epsilon-connected ordinal natural set

((A) *^ ((B) *^ (s))) +^ ((A) *^ (((B) *^ (s)) +^ ((B) *^ (s)))) is epsilon-transitive epsilon-connected ordinal natural set

((((A) *^ ((B) *^ (s))) +^ ((A) *^ (((B) *^ (s)) +^ ((B) *^ (s))))),(((A) *^ (B)) *^ (s))) is Element of ()

(A) *^ ((B) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

((((A) *^ ((B) *^ (s))) +^ ((A) *^ (((B) *^ (s)) +^ ((B) *^ (s))))),((A) *^ ((B) *^ (s)))) is Element of ()

((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s))) is Element of ()

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

(((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s))),((A),(A))) is Element of ()

(((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s)))) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(((A),(A))) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s)))) *^ (((A),(A))) is epsilon-transitive epsilon-connected ordinal natural set

(((A),(A))) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s)))) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(((A),(A))) *^ (((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s)))) is epsilon-transitive epsilon-connected ordinal natural set

((((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s)))) *^ (((A),(A)))) +^ ((((A),(A))) *^ (((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s))))) is epsilon-transitive epsilon-connected ordinal natural set

(((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s)))) *^ (((A),(A))) is epsilon-transitive epsilon-connected ordinal natural set

((((((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s)))) *^ (((A),(A)))) +^ ((((A),(A))) *^ (((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s)))))),((((((B) *^ (s)) +^ ((B) *^ (s))),((B) *^ (s)))) *^ (((A),(A))))) is Element of ()

A is Element of ()

B is Element of ()

(A,B) is Element of ()

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

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

(A) *^ (B) is epsilon-transitive epsilon-connected ordinal natural set

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

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

(A) *^ (B) is epsilon-transitive epsilon-connected ordinal natural set

(((A) *^ (B)),((A) *^ (B))) is Element of ()

s is Element of ()

((A,B),s) is Element of ()

((A,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

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

((A,B)) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

((A,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

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

((A,B)) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

((((A,B)) *^ (s)),(((A,B)) *^ (s))) is Element of ()

(B,s) is Element of ()

(B) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

(B) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

(((B) *^ (s)),((B) *^ (s))) is Element of ()

(A,(B,s)) is Element of ()

((B,s)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A) *^ ((B,s)) is epsilon-transitive epsilon-connected ordinal natural set

((B,s)) is epsilon-transitive epsilon-connected ordinal natural Element of omega

(A) *^ ((B,s)) is epsilon-transitive epsilon-connected ordinal natural set

(((A) *^ ((B,s))),((A) *^ ((B,s)))) is Element of ()

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

((s),(s)) is Element of ()

((A) *^ (B)) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

((A) *^ (B)) *^ (s) is epsilon-transitive epsilon-connected ordinal natural set

((((A) *^ (B)) *^ (s)),(((A) *^ (B)) *^ (s))) is Element of ()

(A) *^ ((B) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

(((A) *^ ((B) *^ (s))),(((A) *^ (B)) *^ (s))) is Element of ()

(A) *^ ((B) *^ (s)) is epsilon-transitive epsilon-connected ordinal natural set

(((A) *^ ((B) *^ (s))),((A) *^ ((B) *^ (s)))) is Element of ()

() is non empty epsilon-transitive epsilon-connected ordinal natural Element of ()

A is Element of ()

(A,()) is Element of ()

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

(()) is epsilon-transitive epsilon-connected ordinal natural Element of omega

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

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

(()) is epsilon-transitive epsilon-connected ordinal natural Element of omega

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

(((A) *^ (())),((A) *^ (()))) is Element of ()

(A) *^ 1 is epsilon-transitive epsilon-connected ordinal natural set

(A) *^ 1 is epsilon-transitive epsilon-connected ordinal natural set

A is Element of ()

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

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

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

c

(A,c

(c

(A) *^ (c

(c

(A) *^ (c

(((A) *^ (c

A is Element of ()

B is Element of ()

c

(A,c

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

(c

(A) *^ (c

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

(c

(A) *^ (c

(((A) *^ (c

(c

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

(c

(B) is epsilon-transitive epsilon-connected ordinal natural Element of o