:: 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

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

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

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
{ b1 where b1 is Element of K26(m) : len b1 = r } is set
r is V14() non finite 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
{ b1 where b1 is Element of K26(r) : len b1 = m } is set

r is set
X is set
K27(r,X) is Relation-like set
K26(K27(r,X)) is non empty 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
{ b1 where b1 is Element of K26(r) : len b1 = m } 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
{ b1 where b1 is Element of K26(X) : len b1 = m } is set
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

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

dom h is set
rng h is set

dom h is set
rng h is set
S is Element of K26(X)

h is Element of K26(r)

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
{ b1 where b1 is Element of K26(m) : len b1 = X } is set
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
{ b1 where b1 is Element of K26(r) : len b1 = X } is set
P is set
X9 is Element of K26(m)

P9 is Element of K26(r)

r is set
K26(r) is non empty set

X is set
K27(r,X) is Relation-like set
K26(K27(r,X)) is non empty set

(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
{ b1 where b1 is Element of K26(r) : len b1 = m } 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
{ b1 where b1 is Element of K26(X) : len b1 = m } is set
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
{ b1 where b1 is Element of K26((P .: X9)) : len b1 = m } is set
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
{ b1 where b1 is Element of K26(X9) : len b1 = m } is set
(m,r,X,P) .: (the_subsets_of_card (m,X9)) is set

P9 .: r is set
Funcs (r,X) is functional set

dom F1 is set
rng F1 is set

F1 .: X is set
P9 .: (F1 .: X) is 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)

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

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

dom h is set
rng h is set
S is Element of K26((P .: X9))

h is Element of K26(X9)

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
{ b1 where b1 is Element of K26(m) : len b1 = 0 } is set
r is set
X is Element of K26(m)

X is Element of K26(m)

r is finite V143() set

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
{ b1 where b1 is Element of K26(r) : len b1 = m } is set
{r} is non empty V14() finite V36() 1 -element V143() set
X is set
P is finite V143() Element of K26(r)

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 r) - (card X9) is V16() V17() ext-real set
P is finite V143() Element of K26(r)
m is set

m is set
r is set
m \/ r is 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

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
{ b1 where b1 is Element of K26(X) : len b1 = m } is set
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

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
{ b1 where b1 is Element of K26(P9) : len b1 = P + 1 } is 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

the_subsets_of_card (omega,P9) is Element of K26(K26(P9))
{ b1 where b1 is Element of K26(P9) : len b1 = omega } is set
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))

S is 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
{ b1 where b1 is Element of K26((S \ {h})) : len b1 = P } is set
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}))

(S \ {h}) \/ {h} is non empty set
S \/ {h} is non empty set
x99 is finite V143() set
x9 is Element of K26(S)

the_subsets_of_card ((P + 1),S) is Element of K26(K26(S))
K26(K26(S)) is non empty set
{ b1 where b1 is Element of K26(S) : len b1 = P + 1 } is set
K27(E,X9) is Relation-like set
K26(K27(E,X9)) is non empty 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
{ b1 where b1 is Element of K26(x9) : len b1 = P } is set
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

h is Element of F1

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
{ b1 where b1 is Element of K26((h \ {E})) : len b1 = P } is set
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)

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
{ b1 where b1 is Element of K26(x) : len b1 = P } is set
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))

{ b1 where b1 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 : ( not b1 <= h & b1 in x ) } is set
min* { b1 where b1 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 : ( not b1 <= h & b1 in 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
x9 is Element of F1
F9 is Element of F1

S9 is Element of F1

{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
{ b1 where b1 is Element of K26((F9 \ {S9})) : len b1 = P } is set
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
{ b1 where b1 is Element of K26(S99) : len b1 = P } is set
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

S999 is V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)
{ b1 where b1 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 : ( b1 <= h & b1 in x ) } is set
s2 is set
S999 \/ { b1 where b1 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 : ( b1 <= h & b1 in x ) } is set

s2 is set

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

{ b2 where b1 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 : ( b2 <= h & b2 in x ) } is set
S999 \/ { b2 where b1 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 : ( b2 <= h & b2 in x ) } is set

{ b2 where b1 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 : ( b2 <= h & b2 in x ) } is set
S999 \/ { b2 where b1 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 : ( b2 <= h & b2 in x ) } is set

{ b2 where b1 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 : ( b2 <= h & b2 in x ) } is set
S999 \/ { b2 where b1 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 : ( b2 <= h & b2 in x ) } is set

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

S99 is Element of F1

c24 is Element of F1
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
{ b1 where b1 is Element of K26((S99 \ {x})) : len b1 = P } is set
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 Element of F1

{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
{ b1 where b1 is Element of K26((F9 \ {S9})) : len b1 = P } is set
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

x is Element of F1

x9 is Element of F1

{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
{ b1 where b1 is Element of K26((x \ {x99})) : len b1 = P } is set
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 . 0 is Element of F1

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

S . E is Element of F1

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

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
{ b1 where b1 is Element of K26((E \ {x9})) : len b1 = P } is set
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

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
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
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
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
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
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
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
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
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 . (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

S . E is Element of F1

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
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
{ b1 where b1 is Element of K26((E \ {x9})) : len b1 = P } is set
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

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
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
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
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
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 . E is Element of F1
S . E is Element of F1

(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

S . h is Element of F1
S . E is Element of F1

S . h is Element of F1
S . E is Element of F1

S . h is Element of F1

{(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
{ b1 where b1 is Element of K26(((S . h) \ {(h . h)})) : len b1 = P } is set
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
{ b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= h )
}
is set

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
{ b1 where b1 is Element of K26(E) : len b1 = P } is set
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

x99 is Element of F1

{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
{ b1 where b1 is Element of K26((x99 \ {F9})) : len b1 = P } is set
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
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
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
{ b1 where b1 is Element of K26(S9) : len b1 = P } is set
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
{ b1 where b1 is Element of K26((S . (h + 1))) : len b1 = P } is set
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

S . c24 is Element of F1
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
c24 is set
(E | (the_subsets_of_card (P,E))) . S99 is set
(E | (the_subsets_of_card (P,E))) . c24 is set
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))))) . c24 is set
((E | (the_subsets_of_card (P,(S . (h + 1))))) | (the_subsets_of_card (P,E))) . c24 is set
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

{ b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= h )
}
is set

len { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= h )
}
is epsilon-transitive epsilon-connected ordinal cardinal set

E is set

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)
() \ (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 set
(h | (NAT \ (Segm (h + 1)))) . x is set

h is set

S . E is Element of F1

S . (E + 1) is Element of F1
{ b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
is set

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
{ b1 where b1 is Element of K26(((S . E) \ {x})) : len b1 = P } is set
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)

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
{ b1 where b1 is Element of K26(F9) : len b1 = P } is set
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, { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
) is Element of K26(K26( { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
))

K26( { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
) is non empty set

K26(K26( { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
)) is non empty set

{ b1 where b1 is Element of K26( { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
) : len b1 = P
}
is set

x99 | (the_subsets_of_card (P, { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
)
)
is Relation-like the_subsets_of_card (P,((S . E) \ {x})) -defined the_subsets_of_card (P, { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
) -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))

K27((the_subsets_of_card (P, { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
)
)
,X9) is Relation-like set

K26(K27((the_subsets_of_card (P, { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
)
)
,X9)) is non empty set

len { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
is epsilon-transitive epsilon-connected ordinal cardinal set

rng (x99 | (the_subsets_of_card (P, { b1 where b1 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 : ex b2 being 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 st
( h . b2 = b1 & not b2 <= E )
}
)
)
)
is set

{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
{ b1 where b1 is Element of K26(S99) : len b1 = P } is set

S . c24 is Element of F1

{(h . c24)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
(S . c24) \ {(h . c24)} is Element of K26((S . c24))
K26((S . c24)) is non empty set
the_subsets_of_card (P,((S . c24) \ {(h . c24)})) is Element of K26(K26(((S . c24) \ {(h . c24)})))
K26(((S . c24) \ {(h . c24)})) is non empty set
K26(K26(((S . c24) \ {(h . c24)}))) is non empty set
{ b1 where b1 is Element of K26(((S . c24) \ {(h . c24)})) : len b1 = P } is set
K27((the_subsets_of_card (P,((S . c24) \ {(h . c24)}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,((S . c24) \ {(h . c24)}))),X9)) is non empty set
{ b1 where b1 is epsilon-transitive epsilon-connected