:: ZFMODEL1 semantic presentation

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()

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()

K139(K45(),K139(K45(),<*1*>,<*(x. 2)*>),<*()*>) 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. 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. 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. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' ()) '&' ('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*>,((x. 2) 'in' ())) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 2) 'in' ())),('not' ((x. 2) 'in' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (((x. 2) 'in' ()) '&' ('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' ()) '&' ('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' ()) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()

K139(K45(),<*2*>,((x. 2) 'in' ())) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' (x. 1)) '&' ('not' ((x. 2) 'in' ())) 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' ()))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (((x. 2) 'in' (x. 1)) '&' ('not' ((x. 2) 'in' ()))) 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' ())))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(((x. 2) 'in' ()) => ((x. 2) 'in' (x. 1))) '&' (((x. 2) 'in' (x. 1)) => ((x. 2) 'in' ())) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),<*3*>,(((x. 2) 'in' ()) => ((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. 2) 'in' (x. 1)))),(((x. 2) 'in' (x. 1)) => ((x. 2) 'in' ()))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((x. 2),(((x. 2) 'in' ()) <=> ((x. 2) 'in' (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)*>),(((x. 2) 'in' ()) <=> ((x. 2) 'in' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()

K139(K45(),K139(K45(),,<*()*>),<*(x. 1)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(All ((x. 2),(((x. 2) 'in' ()) <=> ((x. 2) 'in' (x. 1))))) => (() '=' (x. 1)) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()

K139(K45(),<*2*>,(() '=' (x. 1))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(All ((x. 2),(((x. 2) 'in' ()) <=> ((x. 2) 'in' (x. 1))))) '&' ('not' (() '=' (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. 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. 2) 'in' (x. 1)))))),('not' (() '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' ((All ((x. 2),(((x. 2) 'in' ()) <=> ((x. 2) 'in' (x. 1))))) '&' ('not' (() '=' (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. 2) 'in' (x. 1))))) '&' ('not' (() '=' (x. 1))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((),(x. 1),((All ((x. 2),(((x. 2) 'in' ()) <=> ((x. 2) 'in' (x. 1))))) => (() '=' (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. 2) 'in' (x. 1))))) => (() '=' (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)*>),((All ((x. 2),(((x. 2) 'in' ()) <=> ((x. 2) 'in' (x. 1))))) => (() '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((),(All ((x. 1),((All ((x. 2),(((x. 2) 'in' ()) <=> ((x. 2) 'in' (x. 1))))) => (() '=' (x. 1)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()

K139(K45(),K139(K45(),<*4*>,<*()*>),(All ((x. 1),((All ((x. 2),(((x. 2) 'in' ()) <=> ((x. 2) 'in' (x. 1))))) => (() '=' (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 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)) . () 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)) . () is Element of E

K139(K45(),K139(K45(),<*1*>,<*(x. 3)*>),<*(x. 2)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()

K139(K45(),K139(K45(),,<*(x. 3)*>),<*()*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()

K139(K45(),K139(K45(),,<*(x. 3)*>),<*(x. 1)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 3) '=' ()) '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) '=' ())) is Relation-like K45() -defined K45() -valued Function-like FinSequence-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) '=' ())) '&' ('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) '=' ()))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,('not' ((x. 3) '=' ()))),('not' ((x. 3) '=' (x. 1)))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
'not' (('not' ((x. 3) '=' ())) '&' ('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) '=' ())) '&' ('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) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) 'or' ((x. 3) '=' (x. 1)))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(((x. 3) '=' ()) '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(),<*2*>,((x. 3) 'in' (x. 2))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
(((x. 3) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) 'or' ((x. 3) '=' (x. 1)))) '&' ((((x. 3) '=' ()) '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) '=' ()) '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) '=' ()) 'or' ((x. 3) '=' (x. 1))))),((((x. 3) '=' ()) '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) '=' ()) '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. 3)*>),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) '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) '=' ()) 'or' ((x. 3) '=' (x. 1)))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((),(x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) '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) '=' ()) '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) '=' ()) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((),(All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) '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*>,<*()*>),(All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) '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

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:] +* ((),v)) +* ((x. 1),a) 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:] +* ((),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:] +* ((),v)) . () is Element of E
(( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:] +* ((),v)) +* ((x. 1),a)) . () 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)) . () is Element of E
(i +* ((x. 3),m1)) . (x. 1) is Element of E
i . (x. 1) is Element of E
i . () 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)) . () is Element of E
i . () 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

v . () is Element of E
v . (x. 1) is Element of E
{(v . ()),(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)) . () is Element of E
(v +* ((x. 2),a)) . (x. 1) is Element of E

u . (x. 3) is Element of E
u . (x. 2) is Element of E
u . (x. 1) is Element of E
u . () 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

K139(K45(),K139(K45(),<*1*>,<*(x. 2)*>),<*(x. 3)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()

K139(K45(),K139(K45(),<*1*>,<*(x. 3)*>),<*()*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ()) 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' ())) 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' ()))) 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' ())) 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' ()))) 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' ())))) 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' ())))) 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' ()))))) 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' ())))))) 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' ())))) 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' ())))) 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' ())))) 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' ()))))) 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' ()))))) 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' ())))))) 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' ())))))) 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' ()))))))) 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. 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' ())))) '&' ('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' ()))))) 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' ()))))),('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' ())))) '&' ('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' ())))) '&' ('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' ()))))) '&' ((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))) => ((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' ())))))) 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' ())))))),((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))) => ((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' ())))))) 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' ())))))) 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' ())))))))) 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' ()))))))) 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' ())))))))) 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' ()))))))))) 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' ()))))))))) 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' ())))))))))) 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' ()))))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
All ((),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))))))))) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()
K139(K45(),K139(K45(),<*4*>,<*()*>),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))))))))) 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

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:] +* ((),v)) . () is Element of E
e . (x. 1) is Element of E
u is set
e . () 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 Element of E
(e +* ((x. 2),i)) . () 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)) . () is Element of E
(e +* ((x. 2),m1)) . () 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 Element of E
union (u . ()) 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 . (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)) . () is Element of E
(e +* ((x. 3),i)) . (x. 2) is Element of E
(e +* ((x. 3),i)) . () is Element of E
e . () 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 . (x. 3) is Element of E
u . () is Element of E
u . (x. 2) is Element of E
union (u . ()) is set
e . () is Element of E
(u +* ((x. 1),v)) . () 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

K139(K45(),K139(K45(),<*1*>,<*(x. 1)*>),<*()*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()

K139(K45(),K139(K45(),,<*(x. 3)*>),<*(x. 2)*>) is Relation-like K45() -defined K45() -valued Function-like FinSequence-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' ()) '&' ('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' ())) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 3) 'in' ())),('not' ((x. 3) '=' (x. 2)))) 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()

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()

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(),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' ()) '&' ('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' ()) '&' ('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' ()) '&' ('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' ()) '&' ('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' ()) '&' ('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' ()) '&' ('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' ()) '&' ('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' ()) '&' ('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' ()) '&' ('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' ()) '&' ('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' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' ('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' ()) '&' ('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' ()) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ())),('not' (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ())) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like FinSequence of K45()
K139(K45(),K139(K45(),<*3*>,((x. 1) 'in' ())),(All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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. 1),(((x. 1) 'in' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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 ((),(Ex ((x. 1),(((x. 1) 'in' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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 ((),('not' (Ex ((x. 1),(((x. 1) 'in' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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*>,<*()*>),('not' (Ex ((x. 1),(((x. 1) 'in' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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 ((),('not' (Ex ((x. 1),(((x. 1) 'in' ()) '&' (All ((x. 2),(((x. 2) 'in' ()) => (Ex ((x. 3),((((x. 3) 'in' ()) '&' ('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

v . () 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)) . () is Element of E

i . () 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 +* ((),u) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
a is Element of E
(e +* ((),u)) +* ((x. 1),a) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of bool [:VAR,E:]
(e +* ((),u)) . () is Element of E

j . (x. 2) is Element of E
j . () is Element of E
((e +* ((),u)) +* ((x. 1),a)) . () 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 . (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)) . () 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 +* ((),u)) +* ((x. 1),a)) . (x. 1) is Element of E
j is ext-real natural V14() Element of VAR
((e +* ((),u)) +* ((x. 1),a)) . j is Element of E
(e +* ((),u)) . j is Element of E
j is ext-real natural V14() Element of VAR
(e +* ((),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

((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()) is Relation-like K45() -defined K45() -valued Function-like FinSequence-like ZF-formula-like FinSequence of K45()