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