K41() is V32() V33() V34() V38() set
K45() is V32() V33() V34() V35() V36() V37() V38() Element of bool K41()
bool K41() is non empty set
omega is V32() V33() V34() V35() V36() V37() V38() set
bool omega is non empty set
bool K45() is non empty set
VAR is non empty V32() V33() V34() V35() V36() V37() Element of bool K45()
5 is ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() Element of K45()
{ b1 where b1 is ext-real natural V14() V32() V33() V34() V35() V36() V37() Element of K45() : 5 <= b1 } is set
bool VAR is non empty set
{} is set
the empty Relation-like non-empty empty-yielding V32() V33() V34() V35() V36() V37() V38() set is empty Relation-like non-empty empty-yielding V32() V33() V34() V35() V36() V37() V38() set
0 is ext-real natural V14() V32() V33() V34() V35() V36() V37() Element of K45()
x. 0 is ext-real natural V14() Element of VAR
5 + 0 is ext-real natural V14() V32() V33() V34() V35() V36() V37() Element of K45()
1 is ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() Element of K45()
x. 1 is ext-real natural V14() Element of VAR
5 + 1 is ext-real natural V14() V32() V33() V34() V35() V36() V37() Element of K45()
2 is ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() Element of K45()
x. 2 is ext-real natural V14() Element of VAR
5 + 2 is ext-real natural V14() V32() V33() V34() V35() V36() V37() Element of K45()
3 is ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() Element of K45()
x. 3 is ext-real natural V14() Element of VAR
5 + 3 is ext-real natural V14() V32() V33() V34() V35() V36() V37() Element of K45()
4 is ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() Element of K45()
x. 4 is ext-real natural V14() Element of VAR
5 + 4 is ext-real natural V14() V32() V33() V34() V35() V36() V37() Element of K45()
the_axiom_of_extensionality is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
(x. 2) 'in' (x. 0) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
<*1*> is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
<*(x. 2)*> is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),<*1*>,<*(x. 2)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
<*(x. 0)*> is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*1*>,<*(x. 2)*>),<*(x. 0)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(x. 2) 'in' (x. 1) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
<*(x. 1)*> is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*1*>,<*(x. 2)*>),<*(x. 1)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' ((x. 2) 'in' (x. 1)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
<*2*> is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),<*2*>,((x. 2) 'in' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' (x. 0)) '&' ('not' ((x. 2) 'in' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
<*3*> is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),<*3*>,((x. 2) 'in' (x. 0))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 2) 'in' (x. 0))),('not' ((x. 2) 'in' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (((x. 2) 'in' (x. 0)) '&' ('not' ((x. 2) 'in' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(((x. 2) 'in' (x. 0)) '&' ('not' ((x. 2) 'in' (x. 1))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' (x. 1)) => ((x. 2) 'in' (x. 0)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' ((x. 2) 'in' (x. 0)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,((x. 2) 'in' (x. 0))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' (x. 1)) '&' ('not' ((x. 2) 'in' (x. 0))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,((x. 2) 'in' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 2) 'in' (x. 1))),('not' ((x. 2) 'in' (x. 0)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (((x. 2) 'in' (x. 1)) '&' ('not' ((x. 2) 'in' (x. 0)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(((x. 2) 'in' (x. 1)) '&' ('not' ((x. 2) 'in' (x. 0))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))) '&' (((x. 2) 'in' (x. 1)) => ((x. 2) 'in' (x. 0))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1)))),(((x. 2) 'in' (x. 1)) => ((x. 2) 'in' (x. 0)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
<*4*> is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),<*4*>,<*(x. 2)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 2)*>),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(x. 0) '=' (x. 1) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
<*0*> is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),<*0*>,<*(x. 0)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*0*>,<*(x. 0)*>),<*(x. 1)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' ((x. 0) '=' (x. 1)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,((x. 0) '=' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) '&' ('not' ((x. 0) '=' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,(All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,(All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))))),('not' ((x. 0) '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' ((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) '&' ('not' ((x. 0) '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) '&' ('not' ((x. 0) '=' (x. 1))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 0),(x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
All ((x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*4*>,<*(x. 1)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 1)*>),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 0),(All ((x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*4*>,<*(x. 0)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 0)*>),(All ((x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
E is non empty set
[:VAR,E:] is non empty Relation-like set
bool [:VAR,E:] is non empty set
u is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
u . (x. 0) is Element of E
u . (x. 1) is Element of E
v is set
a is Element of E
u +* ((x. 2),a) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(u +* ((x. 2),a)) . (x. 1) is Element of E
u is ext-real natural V14() Element of VAR
(u +* ((x. 2),a)) . u is Element of E
u . u is Element of E
(u +* ((x. 2),a)) . (x. 2) is Element of E
(u +* ((x. 2),a)) . (x. 0) is Element of E
v is set
a is Element of E
u +* ((x. 2),a) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(u +* ((x. 2),a)) . (x. 1) is Element of E
u is ext-real natural V14() Element of VAR
(u +* ((x. 2),a)) . u is Element of E
u . u is Element of E
(u +* ((x. 2),a)) . (x. 2) is Element of E
(u +* ((x. 2),a)) . (x. 0) is Element of E
the_axiom_of_pairs is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
(x. 3) 'in' (x. 2) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
<*(x. 3)*> is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),<*1*>,<*(x. 3)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*1*>,<*(x. 3)*>),<*(x. 2)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(x. 3) '=' (x. 0) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*0*>,<*(x. 3)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*0*>,<*(x. 3)*>),<*(x. 0)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(x. 3) '=' (x. 1) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*0*>,<*(x. 3)*>),<*(x. 1)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' ((x. 3) '=' (x. 0)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,((x. 3) '=' (x. 0))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' ((x. 3) '=' (x. 1)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,((x. 3) '=' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
('not' ((x. 3) '=' (x. 0))) '&' ('not' ((x. 3) '=' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,('not' ((x. 3) '=' (x. 0)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,('not' ((x. 3) '=' (x. 0)))),('not' ((x. 3) '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (('not' ((x. 3) '=' (x. 0))) '&' ('not' ((x. 3) '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(('not' ((x. 3) '=' (x. 0))) '&' ('not' ((x. 3) '=' (x. 1))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,((x. 3) 'in' (x. 2))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 3) 'in' (x. 2))),('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) => ((x. 3) 'in' (x. 2)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' ((x. 3) 'in' (x. 2)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,((x. 3) 'in' (x. 2))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))),('not' ((x. 3) 'in' (x. 2)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' ((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) '&' ((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) => ((x. 3) 'in' (x. 2))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,(((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,(((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))),((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) => ((x. 3) 'in' (x. 2)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*4*>,<*(x. 3)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 3)*>),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 2)*>),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 0),(x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 1)*>),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 0),(All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 0)*>),(All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
E is non empty set
u is set
v is Element of E
[:VAR,E:] is non empty Relation-like set
bool [:VAR,E:] is non empty set
the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:] is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
v is Element of E
a is Element of E
{v,a} is set
the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:] +* ((x. 0),v) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:] +* ((x. 0),v)) +* ((x. 1),a) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
i is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:] +* ((x. 0),v)) +* ((x. 1),a)) . (x. 1) is Element of E
( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:] +* ((x. 0),v)) . (x. 0) is Element of E
(( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:] +* ((x. 0),v)) +* ((x. 1),a)) . (x. 0) is Element of E
i . (x. 2) is Element of E
j is set
m1 is Element of E
i +* ((x. 3),m1) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(i +* ((x. 3),m1)) . (x. 3) is Element of E
k is ext-real natural V14() Element of VAR
(i +* ((x. 3),m1)) . k is Element of E
i . k is Element of E
(i +* ((x. 3),m1)) . (x. 2) is Element of E
(i +* ((x. 3),m1)) . (x. 0) is Element of E
(i +* ((x. 3),m1)) . (x. 1) is Element of E
i . (x. 1) is Element of E
i . (x. 0) is Element of E
m1 is Element of E
i +* ((x. 3),m1) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(i +* ((x. 3),m1)) . (x. 3) is Element of E
k is ext-real natural V14() Element of VAR
(i +* ((x. 3),m1)) . k is Element of E
i . k is Element of E
(i +* ((x. 3),m1)) . (x. 1) is Element of E
i . (x. 1) is Element of E
(i +* ((x. 3),m1)) . (x. 0) is Element of E
i . (x. 0) is Element of E
(i +* ((x. 3),m1)) . (x. 2) is Element of E
[:VAR,E:] is non empty Relation-like set
bool [:VAR,E:] is non empty set
u is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
v is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
v . (x. 0) is Element of E
v . (x. 1) is Element of E
{(v . (x. 0)),(v . (x. 1))} is set
a is Element of E
v +* ((x. 2),a) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(v +* ((x. 2),a)) . (x. 2) is Element of E
(v +* ((x. 2),a)) . (x. 0) is Element of E
(v +* ((x. 2),a)) . (x. 1) is Element of E
u is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
u . (x. 3) is Element of E
u . (x. 2) is Element of E
u . (x. 1) is Element of E
u . (x. 0) is Element of E
u is ext-real natural V14() Element of VAR
(v +* ((x. 2),a)) . u is Element of E
v . u is Element of E
E is non empty set
u is set
v is set
{u,v} is set
u is Element of E
v is Element of E
{u,v} is set
the_axiom_of_unions is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
(x. 2) 'in' (x. 3) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*1*>,<*(x. 2)*>),<*(x. 3)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(x. 3) 'in' (x. 0) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*1*>,<*(x. 3)*>),<*(x. 0)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,((x. 2) 'in' (x. 3))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 2) 'in' (x. 3))),((x. 3) 'in' (x. 0))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 3)*>),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 2) 'in' (x. 1))),('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))),('not' ((x. 2) 'in' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' ((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) '&' ((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,(((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,(((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))),((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 2)*>),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 1)*>),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 0),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 0)*>),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
E is non empty set
[:VAR,E:] is non empty Relation-like set
bool [:VAR,E:] is non empty set
the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:] is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
v is Element of E
union v is set
the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:] +* ((x. 0),v) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
e is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:] +* ((x. 0),v)) . (x. 0) is Element of E
e . (x. 1) is Element of E
u is set
e . (x. 0) is Element of E
i is Element of E
e +* ((x. 2),i) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(e +* ((x. 2),i)) . (x. 2) is Element of E
m1 is ext-real natural V14() Element of VAR
(e +* ((x. 2),i)) . m1 is Element of E
e . m1 is Element of E
(e +* ((x. 2),i)) . (x. 1) is Element of E
m1 is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
m1 . (x. 0) is Element of E
(e +* ((x. 2),i)) . (x. 0) is Element of E
m1 . (x. 2) is Element of E
m1 . (x. 3) is Element of E
m is set
i is set
j is Element of E
m1 is Element of E
e +* ((x. 2),m1) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(e +* ((x. 2),m1)) +* ((x. 3),j) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
((e +* ((x. 2),m1)) +* ((x. 3),j)) . (x. 3) is Element of E
((e +* ((x. 2),m1)) +* ((x. 3),j)) . (x. 0) is Element of E
(e +* ((x. 2),m1)) . (x. 0) is Element of E
(e +* ((x. 2),m1)) . (x. 2) is Element of E
x is ext-real natural V14() Element of VAR
(e +* ((x. 2),m1)) . x is Element of E
e . x is Element of E
((e +* ((x. 2),m1)) +* ((x. 3),j)) . (x. 2) is Element of E
x is ext-real natural V14() Element of VAR
((e +* ((x. 2),m1)) +* ((x. 3),j)) . x is Element of E
(e +* ((x. 2),m1)) . x is Element of E
(e +* ((x. 2),m1)) . (x. 1) is Element of E
[:VAR,E:] is non empty Relation-like set
bool [:VAR,E:] is non empty set
u is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
u . (x. 0) is Element of E
union (u . (x. 0)) is set
v is Element of E
u +* ((x. 1),v) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(u +* ((x. 1),v)) . (x. 1) is Element of E
e is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
e . (x. 1) is Element of E
e . (x. 2) is Element of E
u is set
i is Element of E
e +* ((x. 3),i) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(e +* ((x. 3),i)) . (x. 3) is Element of E
(u +* ((x. 1),v)) . (x. 0) is Element of E
(e +* ((x. 3),i)) . (x. 2) is Element of E
(e +* ((x. 3),i)) . (x. 0) is Element of E
e . (x. 0) is Element of E
m1 is ext-real natural V14() Element of VAR
(e +* ((x. 3),i)) . m1 is Element of E
e . m1 is Element of E
u is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
u . (x. 3) is Element of E
u . (x. 0) is Element of E
u . (x. 2) is Element of E
union (u . (x. 0)) is set
e . (x. 0) is Element of E
(u +* ((x. 1),v)) . (x. 0) is Element of E
e . (x. 2) is Element of E
e is ext-real natural V14() Element of VAR
(u +* ((x. 1),v)) . e is Element of E
u . e is Element of E
E is non empty set
u is set
union u is set
u is Element of E
union u is set
the_axiom_of_infinity is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
(x. 1) 'in' (x. 0) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*1*>,<*(x. 1)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*1*>,<*(x. 1)*>),<*(x. 0)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(x. 3) '=' (x. 2) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*0*>,<*(x. 3)*>),<*(x. 2)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' ((x. 3) '=' (x. 2)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,((x. 3) '=' (x. 2))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,((x. 3) 'in' (x. 0))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 3) 'in' (x. 0))),('not' ((x. 3) '=' (x. 2)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(x. 4) 'in' (x. 2) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
<*(x. 4)*> is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),<*1*>,<*(x. 4)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*1*>,<*(x. 4)*>),<*(x. 2)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(x. 4) 'in' (x. 3) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*1*>,<*(x. 4)*>),<*(x. 3)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' ((x. 4) 'in' (x. 3)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,((x. 4) 'in' (x. 3))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,((x. 4) 'in' (x. 2))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 4) 'in' (x. 2))),('not' ((x. 4) 'in' (x. 3)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*4*>,<*(x. 4)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 4)*>),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,(((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,(((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2))))),(All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 3),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 3)*>),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (All ((x. 3),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(All ((x. 3),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' (x. 0)) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 2) 'in' (x. 0))),('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (((x. 2) 'in' (x. 0)) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(((x. 2) 'in' (x. 0)) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 2)*>),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,((x. 1) 'in' (x. 0))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 1) 'in' (x. 0))),(All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
Ex ((x. 0),(x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 1),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 1)*>),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (All ((x. 1),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(All ((x. 1),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
Ex ((x. 0),(Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*2*>,(Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 0),('not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*(x. 0)*>),('not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (All ((x. 0),('not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
E is non empty set
[:VAR,E:] is non empty Relation-like set
bool [:VAR,E:] is non empty set
the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:] is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
v is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
v . (x. 0) is Element of E
a is Element of E
e is Element of E
v +* ((x. 2),e) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
i is ext-real natural V14() Element of VAR
(v +* ((x. 2),e)) . i is Element of E
v . i is Element of E
(v +* ((x. 2),e)) . (x. 2) is Element of E
(v +* ((x. 2),e)) . (x. 0) is Element of E
i is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
i . (x. 0) is Element of E
i . (x. 3) is Element of E
j is Element of E
m1 is set
m is Element of E
i +* ((x. 4),m) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(i +* ((x. 4),m)) . (x. 4) is Element of E
x is ext-real natural V14() Element of VAR
(i +* ((x. 4),m)) . x is Element of E
i . x is Element of E
(i +* ((x. 4),m)) . (x. 2) is Element of E
i . (x. 2) is Element of E
(i +* ((x. 4),m)) . (x. 3) is Element of E
i . (x. 2) is Element of E
u is Element of E
the Element of u is Element of u
[:VAR,E:] is non empty Relation-like set
bool [:VAR,E:] is non empty set
e is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
e +* ((x. 0),u) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
a is Element of E
(e +* ((x. 0),u)) +* ((x. 1),a) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(e +* ((x. 0),u)) . (x. 0) is Element of E
j is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
j . (x. 2) is Element of E
j . (x. 0) is Element of E
((e +* ((x. 0),u)) +* ((x. 1),a)) . (x. 0) is Element of E
m1 is Element of E
j +* ((x. 3),m1) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(j +* ((x. 3),m1)) . (x. 3) is Element of E
k is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
k . (x. 4) is Element of E
k . (x. 2) is Element of E
k . (x. 3) is Element of E
(j +* ((x. 3),m1)) . (x. 2) is Element of E
(j +* ((x. 3),m1)) . (x. 0) is Element of E
k is ext-real natural V14() Element of VAR
(j +* ((x. 3),m1)) . k is Element of E
j . k is Element of E
((e +* ((x. 0),u)) +* ((x. 1),a)) . (x. 1) is Element of E
j is ext-real natural V14() Element of VAR
((e +* ((x. 0),u)) +* ((x. 1),a)) . j is Element of E
(e +* ((x. 0),u)) . j is Element of E
j is ext-real natural V14() Element of VAR
(e +* ((x. 0),u)) . j is Element of E
e . j is Element of E
E is non empty set
u is Element of E
v is set
a is set
e is Element of E
u is Element of E
i is set
u is set
v is Element of E
a is Element of E
e is set
u is Element of E
v is Element of E
the_axiom_of_power_sets is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
'not' ((x. 3) 'in' (x. 0)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like