:: ZF_REFLE semantic presentation

REAL is set

K40(REAL) is non empty set

K40(NAT) is non empty V35() set
K40(NAT) is non empty V35() set
VAR is non empty countable Element of K40(NAT)

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT : 5 <= b1 } is set
K40(VAR) is non empty set

x. 0 is Element of VAR

x. 1 is Element of VAR

x. 2 is Element of VAR

x. 3 is Element of VAR

K206(NAT,K210(NAT,1),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K206(NAT,K210(NAT,1),K219((x. 3))),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K210(NAT,0),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K206(NAT,K210(NAT,0),K219((x. 3))),K219(())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K206(NAT,K210(NAT,0),K219((x. 3))),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )

K206(NAT,K210(NAT,2),((x. 3) '=' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K210(NAT,2),((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
('not' ((x. 3) '=' ())) '&' ('not' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )

K206(NAT,K210(NAT,3),('not' ((x. 3) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),('not' ((x. 3) '=' ()))),('not' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (('not' ((x. 3) '=' ())) '&' ('not' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(('not' ((x. 3) '=' ())) '&' ('not' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 3) 'in' (x. 2)) => (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 2))),('not' (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))) => ((x. 3) 'in' (x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )

K206(NAT,K210(NAT,2),((x. 3) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1)))),('not' ((x. 3) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 3) 'in' (x. 2)) => (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )

K206(NAT,K210(NAT,4),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((),(x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219(())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219(())),(All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' ()) 'or' ((x. 3) '=' (x. 1))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K210(NAT,1),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 2))),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K206(NAT,K210(NAT,1),K219((x. 2))),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K206(NAT,K210(NAT,1),K219((x. 3))),K219(())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ()) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 3))),((x. 3) 'in' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ()))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ()))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ()))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 1))),('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))) => ((x. 2) 'in' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )

K206(NAT,K210(NAT,2),((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))) '&' ('not' ((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ()))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ()))))),('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))) '&' ('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))) '&' ('not' ((x. 2) 'in' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' ())))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((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 NAT -defined NAT -valued Function-like V55() M8( NAT )
'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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219(())),(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 NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K210(NAT,1),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 1))),K219(())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K206(NAT,K210(NAT,1),K219((x. 2))),K219(())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K206(NAT,K210(NAT,0),K219((x. 3))),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K210(NAT,2),((x. 3) '=' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' ()) '&' ('not' ((x. 3) '=' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 3) 'in' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' ())),('not' ((x. 3) '=' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
x. 4 is Element of VAR

K206(NAT,K210(NAT,1),K219((x. 4))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 4))),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K206(NAT,K210(NAT,1),K219((x. 4))),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )

K206(NAT,K210(NAT,2),((x. 4) 'in' (x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 4) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) 'in' (x. 2))),('not' ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 4))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 3) 'in' ()) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 3) 'in' ()) '&' ('not' ((x. 3) '=' (x. 2))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((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 NAT -defined NAT -valued Function-like V55() M8( NAT )
'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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
((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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
((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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 2) 'in' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
'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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((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 NAT -defined NAT -valued Function-like V55() M8( NAT )
((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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 1) 'in' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((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 NAT -defined NAT -valued Function-like V55() M8( NAT )
'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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,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 NAT -defined NAT -valued Function-like V55() M8( NAT )
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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219(())),('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 NAT -defined NAT -valued Function-like V55() M8( NAT )
'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 NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )

((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )

K206(NAT,K210(NAT,2),((x. 3) 'in' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 2)) '&' ('not' ((x. 3) 'in' ())) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 2))),('not' ((x. 3) 'in' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 3) 'in' (x. 2)) '&' ('not' ((x. 3) 'in' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 3) 'in' (x. 2)) '&' ('not' ((x. 3) 'in' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) '&' ('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 1))),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 2) 'in' (x. 1)) '&' ('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 2) 'in' (x. 1)) '&' ('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))) => ((x. 2) 'in' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))) '&' ('not' ((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))))),('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))) '&' ('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))) '&' ('not' ((x. 2) 'in' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))))) '&' ((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))) => ((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))))),((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))) => ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ()))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219(())),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' ())))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
{(),(x. 1),(x. 2)} is non empty set

K206(NAT,K210(NAT,0),K219((x. 4))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,0),K219((x. 4))),K219(())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

L is Element of M
M is Element of M
{L,M} is non empty Element of M

L is Element of M
union L is Element of M

L is Element of M
M is Element of M
H is Element of M

{phi} is non empty trivial 1 -element set
phi \/ {phi} is non empty set
a is Element of M
f is Element of M
M is Element of M

L is Element of M
bool L is non empty Element of M
M /\ (bool L) is set

K41(VAR,M) is Relation-like non empty set
K40(K41(VAR,M)) is non empty set

Free L is V35() countable Element of K40(VAR)

K206(NAT,K210(NAT,2),((x. 4) '=' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K206(NAT,K210(NAT,3),L),('not' ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (L '&' ('not' ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(L '&' ('not' ((x. 4) '=' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K210(NAT,3),((x. 4) '=' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) '=' ())),()) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) '=' ()) '&' ()) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) '=' ()) '&' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(L => ((x. 4) '=' ())) '&' (((x. 4) '=' ()) => L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(L => ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(L => ((x. 4) '=' ()))),(((x. 4) '=' ()) => L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(L <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(L <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((),(All ((x. 4),(L <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 4),(L <=> ((x. 4) '=' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 4),(L <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((),('not' (All ((x. 4),(L <=> ((x. 4) '=' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219(())),('not' (All ((x. 4),(L <=> ((x. 4) '=' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((),('not' (All ((x. 4),(L <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((),('not' (All ((x. 4),(L <=> ((x. 4) '=' ())))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(L <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(Ex ((),(All ((x. 4),(L <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

def_func' (L,M) is Relation-like M -defined M -valued Function-like quasi_total Element of K40(K41(M,M))
K41(M,M) is Relation-like non empty set
K40(K41(M,M)) is non empty set
H is Element of M
(def_func' (L,M)) .: H is Element of K40(M)
K40(M) is non empty set

Free L is V35() countable Element of K40(VAR)

K206(NAT,K210(NAT,2),((x. 4) '=' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K206(NAT,K210(NAT,3),L),('not' ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (L '&' ('not' ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(L '&' ('not' ((x. 4) '=' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K210(NAT,3),((x. 4) '=' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) '=' ())),()) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) '=' ()) '&' ()) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) '=' ()) '&' ())) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(L => ((x. 4) '=' ())) '&' (((x. 4) '=' ()) => L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(L => ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(L => ((x. 4) '=' ()))),(((x. 4) '=' ()) => L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(L <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(L <=> ((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((),(All ((x. 4),(L <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 4),(L <=> ((x. 4) '=' ())))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 4),(L <=> ((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((),('not' (All ((x. 4),(L <=> ((x. 4) '=' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219(())),('not' (All ((x. 4),(L <=> ((x. 4) '=' ())))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((),('not' (All ((x. 4),(L <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((),('not' (All ((x. 4),(L <=> ((x. 4) '=' ())))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),(L <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(Ex ((),(All ((x. 4),(L <=> ((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K206(NAT,K210(NAT,1),K219((x. 3))),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )

K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (