:: RAMSEY_1 semantic presentation

REAL is V129() V130() V131() V135() set

NAT is epsilon-transitive epsilon-connected ordinal non empty V14() non finite cardinal limit_cardinal V129() V130() V131() V132() V133() V134() V135() V143() V144() Element of K26(REAL)

K26(REAL) is non empty set

COMPLEX is V129() V135() set

omega is epsilon-transitive epsilon-connected ordinal non empty V14() non finite cardinal limit_cardinal V129() V130() V131() V132() V133() V134() V135() V143() V144() set

K26(omega) is non empty V14() non finite set

K26(NAT) is non empty V14() non finite set

RAT is V129() V130() V131() V132() V135() set

INT is V129() V130() V131() V132() V133() V135() set

K27(REAL,REAL) is Relation-like set

K26(K27(REAL,REAL)) is non empty set

{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() V17() Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V129() V130() V131() V132() V133() V134() V135() V140() V143() set

1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

3 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

len {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() V17() Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V129() V130() V131() V132() V133() V134() V135() V140() V143() set

len omega is epsilon-transitive epsilon-connected ordinal non empty V14() non finite cardinal set

0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() V17() V18() Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V118() V129() V130() V131() V132() V133() V134() V135() V140() V143() Element of NAT

Seg 1 is non empty V14() finite 1 -element V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)

{1} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set

Seg 2 is non empty finite 2 -element V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)

{1,2} is non empty finite V36() V129() V130() V131() V132() V133() V134() V143() set

m is set

K26(m) is non empty set

r is set

the_subsets_of_card (r,m) is Element of K26(K26(m))

K26(K26(m)) is non empty set

{ b

r is V14() non finite set

m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

the_subsets_of_card (m,r) is Element of K26(K26(r))

K26(r) is non empty V14() non finite set

K26(K26(r)) is non empty V14() non finite set

{ b

len r is epsilon-transitive epsilon-connected ordinal V14() non finite cardinal set

card m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

r is set

X is set

K27(r,X) is Relation-like set

K26(K27(r,X)) is non empty set

P is Relation-like r -defined X -valued Function-like quasi_total Element of K26(K27(r,X))

m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

card m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

len r is epsilon-transitive epsilon-connected ordinal cardinal set

the_subsets_of_card (m,r) is Element of K26(K26(r))

K26(r) is non empty set

K26(K26(r)) is non empty set

{ b

the_subsets_of_card (m,X) is Element of K26(K26(X))

K26(X) is non empty set

K26(K26(X)) is non empty set

{ b

K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))) is Relation-like set

K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X)))) is non empty set

P9 is non empty set

F1 is Relation-like Function-like set

dom F1 is set

rng F1 is set

F1 is set

F is set

F1 . F is set

F is Element of P9

P .: F is set

Funcs (r,X) is functional set

rng P is set

h is Relation-like Function-like set

dom h is set

rng h is set

h is Relation-like Function-like set

dom h is set

rng h is set

S is Element of K26(X)

len S is epsilon-transitive epsilon-connected ordinal cardinal set

h is Element of K26(r)

len h is epsilon-transitive epsilon-connected ordinal cardinal set

F1 is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))

F is Element of the_subsets_of_card (m,r)

F1 . F is set

P .: F is set

X9 is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))

P9 is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))

F1 is set

X9 . F1 is set

F1 is Element of the_subsets_of_card (m,r)

P .: F1 is set

P9 . F1 is set

m is set

r is set

X is set

the_subsets_of_card (X,m) is Element of K26(K26(m))

K26(m) is non empty set

K26(K26(m)) is non empty set

{ b

the_subsets_of_card (X,r) is Element of K26(K26(r))

K26(r) is non empty set

K26(K26(r)) is non empty set

{ b

P is set

X9 is Element of K26(m)

len X9 is epsilon-transitive epsilon-connected ordinal cardinal set

P9 is Element of K26(r)

m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

card m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

r is set

K26(r) is non empty set

len r is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

K27(r,X) is Relation-like set

K26(K27(r,X)) is non empty set

P is Relation-like r -defined X -valued Function-like quasi_total Element of K26(K27(r,X))

(m,r,X,P) is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))

the_subsets_of_card (m,r) is Element of K26(K26(r))

K26(K26(r)) is non empty set

{ b

the_subsets_of_card (m,X) is Element of K26(K26(X))

K26(X) is non empty set

K26(K26(X)) is non empty set

{ b

K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))) is Relation-like set

K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X)))) is non empty set

X9 is Element of K26(r)

P .: X9 is set

the_subsets_of_card (m,(P .: X9)) is Element of K26(K26((P .: X9)))

K26((P .: X9)) is non empty set

K26(K26((P .: X9))) is non empty set

{ b

the_subsets_of_card (m,X9) is Element of K26(K26(X9))

K26(X9) is non empty set

K26(K26(X9)) is non empty set

{ b

(m,r,X,P) .: (the_subsets_of_card (m,X9)) is set

P9 is Relation-like Function-like set

P9 .: r is set

Funcs (r,X) is functional set

len X is epsilon-transitive epsilon-connected ordinal cardinal set

F1 is Relation-like Function-like set

dom F1 is set

rng F1 is set

F1 is Relation-like Function-like set

F1 .: X is set

P9 .: (F1 .: X) is set

F1 * P9 is Relation-like Function-like set

(F1 * P9) .: X is set

Funcs ((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))) is functional set

F1 is set

rng P is set

dom (m,r,X,P) is Element of K26((the_subsets_of_card (m,r)))

K26((the_subsets_of_card (m,r))) is non empty set

P " F1 is set

(m,r,X,P) . (P " F1) is set

dom P is Element of K26(r)

P .: (P " F1) is set

F is Element of K26(X9)

len F is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of K26((P .: X9))

len S is epsilon-transitive epsilon-connected ordinal cardinal set

S is Relation-like Function-like set

dom S is set

rng S is set

F is set

(m,r,X,P) . F is set

F is set

(m,r,X,P) . F is set

F is Element of the_subsets_of_card (m,r)

P .: F is set

h is Relation-like Function-like set

dom h is set

rng h is set

S is Element of K26((P .: X9))

len S is epsilon-transitive epsilon-connected ordinal cardinal set

h is Element of K26(X9)

len h is epsilon-transitive epsilon-connected ordinal cardinal set

{0} is non empty V14() functional finite V36() 1 -element V129() V130() V131() V132() V133() V134() V141() V143() set

m is set

the_subsets_of_card (0,m) is Element of K26(K26(m))

K26(m) is non empty set

K26(K26(m)) is non empty set

{ b

r is set

X is Element of K26(m)

len X is epsilon-transitive epsilon-connected ordinal cardinal set

X is Element of K26(m)

len X is epsilon-transitive epsilon-connected ordinal cardinal set

r is finite V143() set

card r is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

m is finite V143() set

the_subsets_of_card (m,r) is finite V36() V143() Element of K26(K26(r))

K26(r) is non empty finite V36() V143() set

K26(K26(r)) is non empty finite V36() V143() set

{ b

{r} is non empty V14() finite V36() 1 -element V143() set

X is set

P is finite V143() Element of K26(r)

card P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

X9 is finite V143() Element of K26(r)

r \ X9 is finite V143() Element of K26(r)

card (r \ X9) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

card X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

(card r) - (card X9) is V16() V17() ext-real set

P is finite V143() Element of K26(r)

m is set

len m is epsilon-transitive epsilon-connected ordinal cardinal set

m is set

r is set

m \/ r is set

len m is epsilon-transitive epsilon-connected ordinal cardinal set

len (m \/ r) is epsilon-transitive epsilon-connected ordinal cardinal set

m is set

r is set

m \ r is Element of K26(m)

K26(m) is non empty set

m \/ r is set

(m \ r) \/ r is set

m is V14() non finite set

r is set

m \/ r is set

m is V14() non finite set

r is finite V143() set

m \ r is Element of K26(m)

K26(m) is non empty V14() non finite set

m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

X is set

the_subsets_of_card (m,X) is Element of K26(K26(X))

K26(X) is non empty set

K26(K26(X)) is non empty set

{ b

K27((the_subsets_of_card (m,X)),r) is Relation-like set

K26(K27((the_subsets_of_card (m,X)),r)) is non empty set

len X is epsilon-transitive epsilon-connected ordinal cardinal set

P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

P + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

P9 is set

the_subsets_of_card ((P + 1),P9) is Element of K26(K26(P9))

K26(P9) is non empty set

K26(K26(P9)) is non empty set

{ b

X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

K27((the_subsets_of_card ((P + 1),P9)),X9) is Relation-like set

K26(K27((the_subsets_of_card ((P + 1),P9)),X9)) is non empty set

len P9 is epsilon-transitive epsilon-connected ordinal cardinal set

the_subsets_of_card (omega,P9) is Element of K26(K26(P9))

{ b

F1 is non empty set

F1 is Relation-like the_subsets_of_card ((P + 1),P9) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card ((P + 1),P9)),X9))

min* P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

S is set

len S is epsilon-transitive epsilon-connected ordinal cardinal set

h is Element of S

{h} is non empty V14() finite 1 -element V143() set

S \ {h} is Element of K26(S)

K26(S) is non empty set

the_subsets_of_card (P,(S \ {h})) is Element of K26(K26((S \ {h})))

K26((S \ {h})) is non empty set

K26(K26((S \ {h}))) is non empty set

{ b

K27((the_subsets_of_card (P,(S \ {h}))),X9) is Relation-like set

K26(K27((the_subsets_of_card (P,(S \ {h}))),X9)) is non empty set

E is non empty set

E is Element of E

E \/ {h} is non empty set

F1 . (E \/ {h}) is set

x is Element of K26((S \ {h}))

len x is epsilon-transitive epsilon-connected ordinal cardinal set

(S \ {h}) \/ {h} is non empty set

S \/ {h} is non empty set

x99 is finite V143() set

x9 is Element of K26(S)

len x9 is epsilon-transitive epsilon-connected ordinal cardinal set

the_subsets_of_card ((P + 1),S) is Element of K26(K26(S))

K26(K26(S)) is non empty set

{ b

K27(E,X9) is Relation-like set

K26(K27(E,X9)) is non empty set

E is Relation-like E -defined X9 -valued Function-like quasi_total Element of K26(K27(E,X9))

len (S \ {h}) is epsilon-transitive epsilon-connected ordinal cardinal set

x is Relation-like the_subsets_of_card (P,(S \ {h})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(S \ {h}))),X9))

x9 is Element of K26((S \ {h}))

the_subsets_of_card (P,x9) is Element of K26(K26(x9))

K26(x9) is non empty set

K26(K26(x9)) is non empty set

{ b

x | (the_subsets_of_card (P,x9)) is Relation-like the_subsets_of_card (P,(S \ {h})) -defined the_subsets_of_card (P,x9) -defined the_subsets_of_card (P,(S \ {h})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(S \ {h}))),X9))

x99 is Element of the_subsets_of_card (P,(S \ {h}))

x . x99 is set

x99 \/ {h} is non empty set

F1 . (x99 \/ {h}) is set

S is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h is Element of F1

h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

E is Element of h

{E} is non empty V14() finite 1 -element V143() set

h \ {E} is Element of K26(h)

K26(h) is non empty set

the_subsets_of_card (P,(h \ {E})) is Element of K26(K26((h \ {E})))

K26((h \ {E})) is non empty set

K26(K26((h \ {E}))) is non empty set

{ b

K27((the_subsets_of_card (P,(h \ {E}))),X9) is Relation-like set

K26(K27((the_subsets_of_card (P,(h \ {E}))),X9)) is non empty set

E is Element of K26(P9)

len E is epsilon-transitive epsilon-connected ordinal cardinal set

x is Element of K26((h \ {E}))

E is Relation-like the_subsets_of_card (P,(h \ {E})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(h \ {E}))),X9))

the_subsets_of_card (P,x) is Element of K26(K26(x))

K26(x) is non empty set

K26(K26(x)) is non empty set

{ b

E | (the_subsets_of_card (P,x)) is Relation-like the_subsets_of_card (P,(h \ {E})) -defined the_subsets_of_card (P,x) -defined the_subsets_of_card (P,(h \ {E})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(h \ {E}))),X9))

len x is epsilon-transitive epsilon-connected ordinal cardinal set

{ b

min* { b

x9 is Element of F1

F9 is Element of F1

S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

S9 is Element of F1

S99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

{S9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set

F9 \ {S9} is Element of K26(F9)

K26(F9) is non empty set

the_subsets_of_card (P,(F9 \ {S9})) is Element of K26(K26((F9 \ {S9})))

K26((F9 \ {S9})) is non empty set

K26(K26((F9 \ {S9}))) is non empty set

{ b

K27((the_subsets_of_card (P,(F9 \ {S9}))),X9) is Relation-like set

K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9)) is non empty set

x is Relation-like the_subsets_of_card (P,(F9 \ {S9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9))

S99 is Element of K26((F9 \ {S9}))

the_subsets_of_card (P,S99) is Element of K26(K26(S99))

K26(S99) is non empty set

K26(K26(S99)) is non empty set

{ b

x | (the_subsets_of_card (P,S99)) is Relation-like the_subsets_of_card (P,(F9 \ {S9})) -defined the_subsets_of_card (P,S99) -defined the_subsets_of_card (P,(F9 \ {S9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9))

S999 is set

s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

S999 is V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)

{ b

s2 is set

S999 \/ { b

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

s2 is set

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

Segm (h + 1) is V129() V130() V131() V132() V133() V134() V143() Element of K26(omega)

s2 is set

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

{ b

S999 \/ { b

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

{ b

S999 \/ { b

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

{ b

S999 \/ { b

s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

s1 is Element of the_subsets_of_card (P,(F9 \ {S9}))

x . s1 is set

s1 \/ {S9} is non empty set

F1 . (s1 \/ {S9}) is set

s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

S99 is Element of F1

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

c

S999 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

{x} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set

S99 \ {x} is Element of K26(S99)

K26(S99) is non empty set

the_subsets_of_card (P,(S99 \ {x})) is Element of K26(K26((S99 \ {x})))

K26((S99 \ {x})) is non empty set

K26(K26((S99 \ {x}))) is non empty set

{ b

K27((the_subsets_of_card (P,(S99 \ {x}))),X9) is Relation-like set

K26(K27((the_subsets_of_card (P,(S99 \ {x}))),X9)) is non empty set

F9 is Element of F1

S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

S9 is Element of F1

S99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

{S9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set

F9 \ {S9} is Element of K26(F9)

K26(F9) is non empty set

the_subsets_of_card (P,(F9 \ {S9})) is Element of K26(K26((F9 \ {S9})))

K26((F9 \ {S9})) is non empty set

K26(K26((F9 \ {S9}))) is non empty set

{ b

K27((the_subsets_of_card (P,(F9 \ {S9}))),X9) is Relation-like set

K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9)) is non empty set

E is Element of F1

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x is Element of F1

x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x9 is Element of F1

F9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

{x99} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set

x \ {x99} is Element of K26(x)

K26(x) is non empty set

the_subsets_of_card (P,(x \ {x99})) is Element of K26(K26((x \ {x99})))

K26((x \ {x99})) is non empty set

K26(K26((x \ {x99}))) is non empty set

{ b

K27((the_subsets_of_card (P,(x \ {x99}))),X9) is Relation-like set

K26(K27((the_subsets_of_card (P,(x \ {x99}))),X9)) is non empty set

K27(NAT,F1) is Relation-like non empty V14() non finite set

K26(K27(NAT,F1)) is non empty V14() non finite set

K27(NAT,omega) is Relation-like non empty V14() non finite set

K26(K27(NAT,omega)) is non empty V14() non finite set

F is Element of F1

S is Relation-like NAT -defined F1 -valued non empty Function-like V25( NAT ) quasi_total Element of K26(K27(NAT,F1))

S . 0 is Element of F1

h is Relation-like NAT -defined omega -valued non empty Function-like V25( NAT ) quasi_total Element of K26(K27(NAT,omega))

h . 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

h . 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

S . (0 + 1) is Element of F1

S . 0 is Element of F1

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

S . E is Element of F1

E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

S . (E + 1) is Element of F1

h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

h . (E + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

E is Element of F1

{x9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set

E \ {x9} is Element of K26(E)

K26(E) is non empty set

the_subsets_of_card (P,(E \ {x9})) is Element of K26(K26((E \ {x9})))

K26((E \ {x9})) is non empty set

K26(K26((E \ {x9}))) is non empty set

{ b

K27((the_subsets_of_card (P,(E \ {x9}))),X9) is Relation-like set

K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9)) is non empty set

x is Element of F1

x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

S9 is Element of K26((E \ {x9}))

F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

the_subsets_of_card (P,S9) is Element of K26(K26(S9))

K26(S9) is non empty set

K26(K26(S9)) is non empty set

{ b

F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

S . (0 + 1) is Element of F1

S9 is Element of K26((E \ {x9}))

F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

the_subsets_of_card (P,S9) is Element of K26(K26(S9))

K26(S9) is non empty set

K26(K26(S9)) is non empty set

{ b

F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

S9 is Element of K26((E \ {x9}))

F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

the_subsets_of_card (P,S9) is Element of K26(K26(S9))

K26(S9) is non empty set

K26(K26(S9)) is non empty set

{ b

F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

S9 is Element of K26((E \ {x9}))

F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

the_subsets_of_card (P,S9) is Element of K26(K26(S9))

K26(S9) is non empty set

K26(K26(S9)) is non empty set

{ b

F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h . (h + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

S . (h + 1) is Element of F1

S . h is Element of F1

h . (h + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

(h + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h . ((h + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

S . ((h + 1) + 1) is Element of F1

S . (h + 1) is Element of F1

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

S . E is Element of F1

E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

S . (E + 1) is Element of F1

h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

h . (E + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

E is Element of F1

x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

{x9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set

E \ {x9} is Element of K26(E)

K26(E) is non empty set

the_subsets_of_card (P,(E \ {x9})) is Element of K26(K26((E \ {x9})))

K26((E \ {x9})) is non empty set

K26(K26((E \ {x9}))) is non empty set

{ b

K27((the_subsets_of_card (P,(E \ {x9}))),X9) is Relation-like set

K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9)) is non empty set

x is Element of F1

x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

S9 is Element of K26((E \ {x9}))

F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

the_subsets_of_card (P,S9) is Element of K26(K26(S9))

K26(S9) is non empty set

K26(K26(S9)) is non empty set

{ b

F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

S9 is Element of K26((E \ {x9}))

F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

the_subsets_of_card (P,S9) is Element of K26(K26(S9))

K26(S9) is non empty set

K26(K26(S9)) is non empty set

{ b

F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))

h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

(h + 1) + E is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real positive non negative V143() set

S . E is Element of F1

S . E is Element of F1

h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

(h + 1) + E is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h + (E + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

S . (E + 1) is Element of F1

h . (E + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

F9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

0 + E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

S . h is Element of F1

S . E is Element of F1

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

S . h is Element of F1

S . E is Element of F1

h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

E + E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

E + x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set

h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

S . h is Element of F1

h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

{(h . h)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set

(S . h) \ {(h . h)} is Element of K26((S . h))

K26((S . h)) is non empty set

the_subsets_of_card (P,((S . h) \ {(h . h)})) is Element of K26(K26(((S . h) \ {(h . h)})))

K26(((S . h) \ {(h . h)})) is non empty set

K26(K26(((S . h) \ {(h . h)}))) is non empty set

{ b

K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9) is Relation-like set

K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9)) is non empty set

{ b

( h . b

h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

S . (h + 1) is Element of F1

E is set

the_subsets_of_card (P,E) is Element of K26(K26(E))

K26(E) is non empty set

K26(K26(E)) is non empty set

{ b

E is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))

E | (the_subsets_of_card (P,E)) is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined the_subsets_of_card (P,E) -defined the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))

h . (h + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x is Element of F1

x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x99 is Element of F1

F9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

{F9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set

x99 \ {F9} is Element of K26(x99)

K26(x99) is non empty set

the_subsets_of_card (P,(x99 \ {F9})) is Element of K26(K26((x99 \ {F9})))

K26((x99 \ {F9})) is non empty set

K26(K26((x99 \ {F9}))) is non empty set

{ b

K27((the_subsets_of_card (P,(x99 \ {F9}))),X9) is Relation-like set

K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9)) is non empty set

S9 is Element of K26((x99 \ {F9}))

S9 is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))

the_subsets_of_card (P,S9) is Element of K26(K26(S9))

K26(S9) is non empty set

K26(K26(S9)) is non empty set

{ b

S9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))

S9 is Element of K26((x99 \ {F9}))

S9 is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))

the_subsets_of_card (P,S9) is Element of K26(K26(S9))

K26(S9) is non empty set

K26(K26(S9)) is non empty set

{ b

S9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))

S99 is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))

S99 is Element of the_subsets_of_card (P,((S . h) \ {(h . h)}))

S99 . S99 is set

E . S99 is set

S99 \/ {(h . h)} is non empty set

F1 . (S99 \/ {(h . h)}) is set

the_subsets_of_card (P,(S . (h + 1))) is Element of K26(K26((S . (h + 1))))

K26((S . (h + 1))) is non empty set

K26(K26((S . (h + 1)))) is non empty set

{ b

E | (the_subsets_of_card (P,(S . (h + 1)))) is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined the_subsets_of_card (P,(S . (h + 1))) -defined the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))

S99 is set

c

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h . x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

c

h . c

S . c

dom (E | (the_subsets_of_card (P,E))) is Element of K26((the_subsets_of_card (P,E)))

K26((the_subsets_of_card (P,E))) is non empty set

S99 is set

c

(E | (the_subsets_of_card (P,E))) . S99 is set

(E | (the_subsets_of_card (P,E))) . c

dom E is Element of K26((the_subsets_of_card (P,((S . h) \ {(h . h)}))))

K26((the_subsets_of_card (P,((S . h) \ {(h . h)})))) is non empty set

dom (E | (the_subsets_of_card (P,(S . (h + 1))))) is Element of K26((the_subsets_of_card (P,((S . h) \ {(h . h)}))))

(E | (the_subsets_of_card (P,(S . (h + 1))))) | (the_subsets_of_card (P,E)) is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined the_subsets_of_card (P,E) -defined the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))

((E | (the_subsets_of_card (P,(S . (h + 1))))) | (the_subsets_of_card (P,E))) . S99 is set

(E | (the_subsets_of_card (P,(S . (h + 1))))) . S99 is set

(E | (the_subsets_of_card (P,(S . (h + 1))))) . c

((E | (the_subsets_of_card (P,(S . (h + 1))))) | (the_subsets_of_card (P,E))) . c

dom h is non empty V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)

h is set

E is set

h . h is set

h . E is set

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h . x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

{ b

( h . b

len { b

( h . b

E is set

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h . x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

Segm (h + 1) is V129() V130() V131() V132() V133() V134() V143() Element of K26(omega)

NAT \ (Segm (h + 1)) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)

h | (NAT \ (Segm (h + 1))) is Relation-like NAT -defined NAT \ (Segm (h + 1)) -defined NAT -defined omega -valued Function-like Element of K26(K27(NAT,omega))

dom (h | (NAT \ (Segm (h + 1)))) is V129() V130() V131() V132() V133() V134() Element of K26((NAT \ (Segm (h + 1))))

K26((NAT \ (Segm (h + 1)))) is non empty set

(dom h) /\ (NAT \ (Segm (h + 1))) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)

NAT /\ (NAT \ (Segm (h + 1))) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)

NAT /\ NAT is V129() V130() V131() V132() V133() V134() Element of K26(REAL)

(NAT /\ NAT) \ (Segm (h + 1)) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)

rng (h | (NAT \ (Segm (h + 1)))) is set

E is set

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h . x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h . x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

x is set

(h | (NAT \ (Segm (h + 1)))) . x is set

x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

h . x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

h is set

E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

S . E is Element of F1

h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT

S . (E + 1) is Element of F1

{ b

( h . b

x is Element of S . E

{x} is non empty V14() finite 1 -element V143() set

(S . E) \ {x} is Element of K26((S . E))

K26((S . E)) is non empty set

the_subsets_of_card (P,((S . E) \ {x})) is Element of K26(K26(((S . E) \ {x})))

K26(((S . E) \ {x})) is non empty set

K26(K26(((S . E) \ {x}))) is non empty set

{ b

K27((the_subsets_of_card (P,((S . E) \ {x}))),X9) is Relation-like set

K26(K27((the_subsets_of_card (P,((S . E) \ {x}))),X9)) is non empty set

x99 is Element of K26(P9)

len x99 is epsilon-transitive epsilon-connected ordinal cardinal set

F9 is Element of K26(((S . E) \ {x}))

x99 is Relation-like the_subsets_of_card (P,((S . E) \ {x})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . E) \ {x}))),X9))

the_subsets_of_card (P,F9) is Element of K26(K26(F9))

K26(F9) is non empty set

K26(K26(F9)) is non empty set

{ b

x99 | (the_subsets_of_card (P,F9)) is Relation-like the_subsets_of_card (P,((S . E) \ {x})) -defined the_subsets_of_card (P,F9) -defined the_subsets_of_card (P,((S . E) \ {x})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . E) \ {x}))),X9))

S9 is set

{(h . E)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set

(S . E) \ {(h . E)} is Element of K26((S . E))

the_subsets_of_card (P, { b

( h . b

( h . b

K26( { b

( h . b

K26(K26( { b

( h . b

{ b

( h . b

x99 | (the_subsets_of_card (P, { b

( h . b

( h . b

K27((the_subsets_of_card (P, { b

( h . b

K26(K27((the_subsets_of_card (P, { b

( h . b

len { b

( h . b

card P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega

rng (x99 | (the_subsets_of_card (P, { b

( h . b

S9 is epsilon-transitive epsilon-connected ordinal Element of X9

{S9} is non empty V14() finite 1 -element V143() set

S9 is set

S99 is set

the_subsets_of_card (P,S99) is Element of K26(K26(S99))

K26(S99) is non empty set

K26(K26(S99)) is non empty set

{ b

c

S . c

h . c

{(h . c

(S . c

K26((S . c

the_subsets_of_card (P,((S . c

K26(((S . c

K26(K26(((S . c

{ b

K27((the_subsets_of_card (P,((S . c

K26(K27((the_subsets_of_card (P,((S . c

{ b