:: 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₆ is epsilon-transitive epsilon-connected ordinal set
s *^ c₆ is epsilon-transitive epsilon-connected ordinal set
c₇ is epsilon-transitive epsilon-connected ordinal set
s *^ c₇ is epsilon-transitive epsilon-connected ordinal set
{} *^ {} 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₆ is epsilon-transitive epsilon-connected ordinal natural set
c₇ is epsilon-transitive epsilon-connected ordinal natural set
s is epsilon-transitive epsilon-connected ordinal natural set
s *^ c₆ is epsilon-transitive epsilon-connected ordinal natural set
s *^ c₇ 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₆ is epsilon-transitive epsilon-connected ordinal natural set
c₇ is epsilon-transitive epsilon-connected ordinal natural set
s is epsilon-transitive epsilon-connected ordinal natural set
s *^ c₆ is epsilon-transitive epsilon-connected ordinal natural set
s *^ c₇ is epsilon-transitive epsilon-connected ordinal natural set
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₆ is epsilon-transitive epsilon-connected ordinal natural Element of omega
1 *^ c₆ is epsilon-transitive epsilon-connected ordinal natural set
c₇ is epsilon-transitive epsilon-connected ordinal set
r is epsilon-transitive epsilon-connected ordinal set
c₇ *^ r is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
c₇ *^ x is epsilon-transitive epsilon-connected ordinal set
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₆ is epsilon-transitive epsilon-connected ordinal natural set
c₆ div^ s is epsilon-transitive epsilon-connected ordinal natural set
s *^ (c₆ div^ s) is epsilon-transitive epsilon-connected ordinal natural set
c₆ mod^ s is epsilon-transitive epsilon-connected ordinal natural set
(s *^ (c₆ div^ s)) +^ (c₆ mod^ s) is epsilon-transitive epsilon-connected ordinal natural set
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₆ div^ s) is epsilon-transitive epsilon-connected ordinal natural set
RATplus *^ ((s div^ RATplus) *^ (c₆ div^ s)) is epsilon-transitive epsilon-connected ordinal natural set
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₆ div^ s) is epsilon-transitive epsilon-connected ordinal natural set
RATplus *^ ((s div^ RATplus) *^ (c₆ div^ s)) 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
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₆ 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 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₆ 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
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₆ is epsilon-transitive epsilon-connected ordinal set
B *^ c₆ is epsilon-transitive epsilon-connected ordinal set
(RATplus,RATplus) *^ (RATplus div^ (RATplus,RATplus)) is epsilon-transitive epsilon-connected ordinal natural set
c₇ is epsilon-transitive epsilon-connected ordinal natural Element of omega
(RATplus,RATplus) *^ c₇ is epsilon-transitive epsilon-connected ordinal natural set
x is epsilon-transitive epsilon-connected ordinal natural Element of omega
((RATplus,RATplus) *^ c₇) *^ x is epsilon-transitive epsilon-connected ordinal natural set
r is epsilon-transitive epsilon-connected ordinal natural Element of omega
((RATplus,RATplus) *^ c₇) *^ r is epsilon-transitive epsilon-connected ordinal natural set
(RATplus,RATplus) div^ ((RATplus,RATplus) *^ c₇) is epsilon-transitive epsilon-connected ordinal natural set
((RATplus,RATplus) *^ c₇) *^ ((RATplus,RATplus) div^ ((RATplus,RATplus) *^ c₇)) is epsilon-transitive epsilon-connected ordinal natural set
c₇ *^ ((RATplus,RATplus) div^ ((RATplus,RATplus) *^ c₇)) is epsilon-transitive epsilon-connected ordinal natural set
(RATplus,RATplus) *^ (c₇ *^ ((RATplus,RATplus) div^ ((RATplus,RATplus) *^ c₇))) is epsilon-transitive epsilon-connected ordinal natural set
(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₆ is epsilon-transitive epsilon-connected ordinal natural Element of omega
c₇ is epsilon-transitive epsilon-connected ordinal natural set
c₆ *^ c₇ 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 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₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( (b₁,b₂) & not b₂ = {} ) } is set
[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₆ is epsilon-transitive epsilon-connected ordinal natural Element of omega
[s,c₆] is set
{s,c₆} is non empty set
{s} is non empty set
{{s,c₆},{s}} is non empty set
{ [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is set
{ [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( (b₁,b₂) & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is Element of K6( { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( (b₁,b₂) & not b₂ = {} ) } )
K6( { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( (b₁,b₂) & not b₂ = {} ) } ) is non empty set
( { [b₁,b₂] where b₁, b₂ is epsilon-transitive epsilon-connected ordinal natural Element of omega : ( (b₁,b₂) & not b₂ = {} ) } \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } ) \/ omega is non empty set
() is set
A is Element of ()
RATplus \ { [b₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is Element of K6(RATplus)
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₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is Element of K6(RATplus)
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₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is Element of K6(RATplus)
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₆ is epsilon-transitive epsilon-connected ordinal natural Element of omega
c₇ is epsilon-transitive epsilon-connected ordinal natural Element of omega
x is epsilon-transitive epsilon-connected ordinal natural set
[c₇,x] is set
{c₇,x} is non empty set
{c₇} is non empty set
{{c₇,x},{c₇}} is non empty set
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₁,1] where b₁ is epsilon-transitive epsilon-connected ordinal natural Element of omega : verum } is Element of K6(RATplus)
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₆ is epsilon-transitive epsilon-connected ordinal natural Element of omega
x is epsilon-transitive epsilon-connected ordinal natural set
c₇ is epsilon-transitive epsilon-connected ordinal natural Element of omega
[x,c₇] is set
{x,c₇} is non empty set
{x} is non empty set
{{x,c₇},{x}} is non empty set
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₆ is epsilon-transitive epsilon-connected ordinal natural set
(c₆,A) is Element of ()
B *^ c₆ is epsilon-transitive epsilon-connected ordinal natural set
((c₆,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((c₆,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₆,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₆,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega
c₆ div^ (c₆,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
(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₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(A,c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
A div^ (A,c₆) 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
((c₆,A)) *^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set
((s,B)) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
(((c₆,A)) *^ (s,B)) *^ ((s,B)) is epsilon-transitive epsilon-connected ordinal natural set
((((c₆,A)) *^ (s,B)) *^ ((s,B))) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
(s,B) *^ ((s,B)) is epsilon-transitive epsilon-connected ordinal natural set
((c₆,A)) *^ ((s,B) *^ ((s,B))) is epsilon-transitive epsilon-connected ordinal natural set
(((c₆,A)) *^ ((s,B) *^ ((s,B)))) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
((c₆,A)) *^ B is epsilon-transitive epsilon-connected ordinal natural set
(((c₆,A)) *^ B) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
((c₆,A)) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
B *^ (((c₆,A)) *^ (A,c₆)) is epsilon-transitive epsilon-connected ordinal natural set
B *^ A is epsilon-transitive epsilon-connected ordinal natural set
((B *^ A),(B *^ c₆)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((B *^ A),(B *^ c₆)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(B *^ A) div^ ((B *^ A),(B *^ c₆)) is epsilon-transitive epsilon-connected ordinal natural set
((B *^ c₆),(B *^ A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((B *^ c₆),(B *^ A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(B *^ c₆) div^ ((B *^ c₆),(B *^ A)) is epsilon-transitive epsilon-connected ordinal natural set
(((c₆,A)),((c₆,A))) is Element of ()
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₆ is Element of ()
(c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
c₇ is Element of ()
(c₇) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₆) *^ (c₇) is epsilon-transitive epsilon-connected ordinal natural set
(c₇) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₇) *^ (c₆) is epsilon-transitive epsilon-connected ordinal natural set
((c₆) *^ (c₇)) +^ ((c₇) *^ (c₆)) is epsilon-transitive epsilon-connected ordinal natural set
(c₆) *^ (c₇) is epsilon-transitive epsilon-connected ordinal natural set
((((c₆) *^ (c₇)) +^ ((c₇) *^ (c₆))),((c₆) *^ (c₇))) is Element of ()
((c₇) *^ (c₆)) +^ ((c₆) *^ (c₇)) is epsilon-transitive epsilon-connected ordinal natural set
(c₇) *^ (c₆) is epsilon-transitive epsilon-connected ordinal natural set
((((c₇) *^ (c₆)) +^ ((c₆) *^ (c₇))),((c₇) *^ (c₆))) is Element of ()
(A) *^ (B) is epsilon-transitive epsilon-connected ordinal natural set
(((A) *^ (B)),((A) *^ (B))) is Element of ()
s is Element of ()
c₆ is Element of ()
(c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
c₇ is Element of ()
(c₇) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₆) *^ (c₇) is epsilon-transitive epsilon-connected ordinal natural set
(c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₇) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₆) *^ (c₇) is epsilon-transitive epsilon-connected ordinal natural set
(((c₆) *^ (c₇)),((c₆) *^ (c₇))) is Element of ()
(c₇) *^ (c₆) is epsilon-transitive epsilon-connected ordinal natural set
(c₇) *^ (c₆) is epsilon-transitive epsilon-connected ordinal natural set
(((c₇) *^ (c₆)),((c₇) *^ (c₆))) is Element of ()
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₆ is epsilon-transitive epsilon-connected ordinal natural set
(c₆,A) is Element of ()
((s,B),(c₆,A)) is Element of ()
((s,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((c₆,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((s,B)) *^ ((c₆,A)) is epsilon-transitive epsilon-connected ordinal natural set
((c₆,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((s,B)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((c₆,A)) *^ ((s,B)) is epsilon-transitive epsilon-connected ordinal natural set
(((s,B)) *^ ((c₆,A))) +^ (((c₆,A)) *^ ((s,B))) is epsilon-transitive epsilon-connected ordinal natural set
((s,B)) *^ ((c₆,A)) is epsilon-transitive epsilon-connected ordinal natural set
(((((s,B)) *^ ((c₆,A))) +^ (((c₆,A)) *^ ((s,B)))),(((s,B)) *^ ((c₆,A)))) is Element of ()
B *^ c₆ is epsilon-transitive epsilon-connected ordinal natural set
(s *^ A) +^ (B *^ c₆) is epsilon-transitive epsilon-connected ordinal natural set
(((s *^ A) +^ (B *^ c₆)),(B *^ A)) is Element of ()
(A,c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(A,c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
A div^ (A,c₆) 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
(c₆,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₆,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega
c₆ div^ (c₆,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
(s,B) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
(B,s) *^ (c₆,A) is epsilon-transitive epsilon-connected ordinal natural set
((s,B) *^ (A,c₆)) +^ ((B,s) *^ (c₆,A)) is epsilon-transitive epsilon-connected ordinal natural set
(((s,B) *^ (A,c₆)) +^ ((B,s) *^ (c₆,A))) *^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set
(B,s) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
((B,s) *^ (A,c₆)) *^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set
(((((s,B) *^ (A,c₆)) +^ ((B,s) *^ (c₆,A))) *^ (s,B)),(((B,s) *^ (A,c₆)) *^ (s,B))) is Element of ()
(B,s) *^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set
(A,c₆) *^ ((B,s) *^ (s,B)) is epsilon-transitive epsilon-connected ordinal natural set
(((((s,B) *^ (A,c₆)) +^ ((B,s) *^ (c₆,A))) *^ (s,B)),((A,c₆) *^ ((B,s) *^ (s,B)))) is Element of ()
(A,c₆) *^ B is epsilon-transitive epsilon-connected ordinal natural set
(((((s,B) *^ (A,c₆)) +^ ((B,s) *^ (c₆,A))) *^ (s,B)),((A,c₆) *^ B)) is Element of ()
((s,B) *^ (A,c₆)) *^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set
((B,s) *^ (c₆,A)) *^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set
(((s,B) *^ (A,c₆)) *^ (s,B)) +^ (((B,s) *^ (c₆,A)) *^ (s,B)) is epsilon-transitive epsilon-connected ordinal natural set
(((((s,B) *^ (A,c₆)) *^ (s,B)) +^ (((B,s) *^ (c₆,A)) *^ (s,B))),((A,c₆) *^ B)) is Element of ()
(s,B) *^ (s,B) is epsilon-transitive epsilon-connected ordinal natural set
(A,c₆) *^ ((s,B) *^ (s,B)) is epsilon-transitive epsilon-connected ordinal natural set
((A,c₆) *^ ((s,B) *^ (s,B))) +^ (((B,s) *^ (c₆,A)) *^ (s,B)) is epsilon-transitive epsilon-connected ordinal natural set
((((A,c₆) *^ ((s,B) *^ (s,B))) +^ (((B,s) *^ (c₆,A)) *^ (s,B))),((A,c₆) *^ B)) is Element of ()
(A,c₆) *^ s is epsilon-transitive epsilon-connected ordinal natural set
((A,c₆) *^ s) +^ (((B,s) *^ (c₆,A)) *^ (s,B)) is epsilon-transitive epsilon-connected ordinal natural set
((((A,c₆) *^ s) +^ (((B,s) *^ (c₆,A)) *^ (s,B))),((A,c₆) *^ B)) is Element of ()
(c₆,A) *^ ((B,s) *^ (s,B)) is epsilon-transitive epsilon-connected ordinal natural set
((A,c₆) *^ s) +^ ((c₆,A) *^ ((B,s) *^ (s,B))) is epsilon-transitive epsilon-connected ordinal natural set
((((A,c₆) *^ s) +^ ((c₆,A) *^ ((B,s) *^ (s,B)))),((A,c₆) *^ B)) is Element of ()
(c₆,A) *^ B is epsilon-transitive epsilon-connected ordinal natural set
((A,c₆) *^ s) +^ ((c₆,A) *^ B) is epsilon-transitive epsilon-connected ordinal natural set
((((A,c₆) *^ s) +^ ((c₆,A) *^ B)),((A,c₆) *^ B)) is Element of ()
(((A,c₆) *^ s) +^ ((c₆,A) *^ B)) *^ (c₆,A) is epsilon-transitive epsilon-connected ordinal natural set
((A,c₆) *^ B) *^ (c₆,A) is epsilon-transitive epsilon-connected ordinal natural set
(((((A,c₆) *^ s) +^ ((c₆,A) *^ B)) *^ (c₆,A)),(((A,c₆) *^ B) *^ (c₆,A))) is Element of ()
(A,c₆) *^ (c₆,A) is epsilon-transitive epsilon-connected ordinal natural set
B *^ ((A,c₆) *^ (c₆,A)) is epsilon-transitive epsilon-connected ordinal natural set
(((((A,c₆) *^ s) +^ ((c₆,A) *^ B)) *^ (c₆,A)),(B *^ ((A,c₆) *^ (c₆,A)))) is Element of ()
(((((A,c₆) *^ s) +^ ((c₆,A) *^ B)) *^ (c₆,A)),(B *^ A)) is Element of ()
((A,c₆) *^ s) *^ (c₆,A) is epsilon-transitive epsilon-connected ordinal natural set
((c₆,A) *^ B) *^ (c₆,A) is epsilon-transitive epsilon-connected ordinal natural set
(((A,c₆) *^ s) *^ (c₆,A)) +^ (((c₆,A) *^ B) *^ (c₆,A)) is epsilon-transitive epsilon-connected ordinal natural set
(((((A,c₆) *^ s) *^ (c₆,A)) +^ (((c₆,A) *^ B) *^ (c₆,A))),(B *^ A)) is Element of ()
s *^ ((A,c₆) *^ (c₆,A)) is epsilon-transitive epsilon-connected ordinal natural set
(s *^ ((A,c₆) *^ (c₆,A))) +^ (((c₆,A) *^ B) *^ (c₆,A)) is epsilon-transitive epsilon-connected ordinal natural set
(((s *^ ((A,c₆) *^ (c₆,A))) +^ (((c₆,A) *^ B) *^ (c₆,A))),(B *^ A)) is Element of ()
(s *^ A) +^ (((c₆,A) *^ B) *^ (c₆,A)) is epsilon-transitive epsilon-connected ordinal natural set
(((s *^ A) +^ (((c₆,A) *^ B) *^ (c₆,A))),(B *^ A)) is Element of ()
(c₆,A) *^ (c₆,A) is epsilon-transitive epsilon-connected ordinal natural set
B *^ ((c₆,A) *^ (c₆,A)) is epsilon-transitive epsilon-connected ordinal natural set
(s *^ A) +^ (B *^ ((c₆,A) *^ (c₆,A))) is epsilon-transitive epsilon-connected ordinal natural set
(((s *^ A) +^ (B *^ ((c₆,A) *^ (c₆,A)))),(B *^ A)) is Element of ()
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₆ is epsilon-transitive epsilon-connected ordinal natural set
(c₆,A) is Element of ()
((B,s),(c₆,A)) is Element of ()
((B,s)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((c₆,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((B,s)) *^ ((c₆,A)) is epsilon-transitive epsilon-connected ordinal natural set
((B,s)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((c₆,A)) is epsilon-transitive epsilon-connected ordinal natural Element of omega
((B,s)) *^ ((c₆,A)) is epsilon-transitive epsilon-connected ordinal natural set
((((B,s)) *^ ((c₆,A))),(((B,s)) *^ ((c₆,A)))) is Element of ()
B *^ c₆ is epsilon-transitive epsilon-connected ordinal natural set
((B *^ c₆),(s *^ A)) is Element of ()
(A,c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(A,c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
A div^ (A,c₆) 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
(c₆,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₆,A) is epsilon-transitive epsilon-connected ordinal natural Element of omega
c₆ div^ (c₆,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) *^ (c₆,A) is epsilon-transitive epsilon-connected ordinal natural set
((B,s) *^ (c₆,A)) *^ (B,s) is epsilon-transitive epsilon-connected ordinal natural set
(s,B) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
((s,B) *^ (A,c₆)) *^ (B,s) is epsilon-transitive epsilon-connected ordinal natural set
((((B,s) *^ (c₆,A)) *^ (B,s)),(((s,B) *^ (A,c₆)) *^ (B,s))) is Element of ()
(B,s) *^ (B,s) is epsilon-transitive epsilon-connected ordinal natural set
(c₆,A) *^ ((B,s) *^ (B,s)) is epsilon-transitive epsilon-connected ordinal natural set
(((c₆,A) *^ ((B,s) *^ (B,s))),(((s,B) *^ (A,c₆)) *^ (B,s))) is Element of ()
(c₆,A) *^ B is epsilon-transitive epsilon-connected ordinal natural set
(((c₆,A) *^ B),(((s,B) *^ (A,c₆)) *^ (B,s))) is Element of ()
(s,B) *^ (B,s) is epsilon-transitive epsilon-connected ordinal natural set
(A,c₆) *^ ((s,B) *^ (B,s)) is epsilon-transitive epsilon-connected ordinal natural set
(((c₆,A) *^ B),((A,c₆) *^ ((s,B) *^ (B,s)))) is Element of ()
(A,c₆) *^ s is epsilon-transitive epsilon-connected ordinal natural set
(((c₆,A) *^ B),((A,c₆) *^ s)) is Element of ()
((c₆,A) *^ B) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
((A,c₆) *^ s) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
((((c₆,A) *^ B) *^ (A,c₆)),(((A,c₆) *^ s) *^ (A,c₆))) is Element of ()
(c₆,A) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
B *^ ((c₆,A) *^ (A,c₆)) is epsilon-transitive epsilon-connected ordinal natural set
((B *^ ((c₆,A) *^ (A,c₆))),(((A,c₆) *^ s) *^ (A,c₆))) is Element of ()
((B *^ c₆),(((A,c₆) *^ s) *^ (A,c₆))) is Element of ()
(A,c₆) *^ (A,c₆) is epsilon-transitive epsilon-connected ordinal natural set
s *^ ((A,c₆) *^ (A,c₆)) is epsilon-transitive epsilon-connected ordinal natural set
((B *^ c₆),(s *^ ((A,c₆) *^ (A,c₆)))) is 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
(()) 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₆ is Element of ()
(A,c₆) is Element of ()
(c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(A) *^ (c₆) is epsilon-transitive epsilon-connected ordinal natural set
(c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(A) *^ (c₆) is epsilon-transitive epsilon-connected ordinal natural set
(((A) *^ (c₆)),((A) *^ (c₆))) is Element of ()
A is Element of ()
B is Element of ()
c₆ is Element of ()
(A,c₆) is Element of ()
(A) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(A) *^ (c₆) is epsilon-transitive epsilon-connected ordinal natural set
(A) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₆) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(A) *^ (c₆) is epsilon-transitive epsilon-connected ordinal natural set
(((A) *^ (c₆)),((A) *^ (c₆))) is Element of ()
(c₆,B) is Element of ()
(B) is epsilon-transitive epsilon-connected ordinal natural Element of omega
(c₆) *^ (B) is epsilon-transitive epsilon-connected ordinal natural set
(B) is epsilon-transitive epsilon-connected ordinal natural Element of o