:: CARD_LAR semantic presentation

REAL is set

NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal limit_cardinal countable denumerable Element of bool REAL

bool REAL is set

NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal limit_cardinal countable denumerable set

bool NAT is non empty non finite set

{} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite cardinal {} -element countable set

1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable Element of NAT

Rank {} is epsilon-transitive set

card {} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite cardinal {} -element countable set

2 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable Element of NAT

0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite cardinal {} -element countable Element of NAT

union {} is epsilon-transitive epsilon-connected ordinal set

dom {} is set

rng {} is set

M is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

card M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

the epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non limit_cardinal non countable regular set is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non limit_cardinal non countable regular set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

sup X is epsilon-transitive epsilon-connected ordinal set

R is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

X /\ R is Element of bool M

sup (X /\ R) is epsilon-transitive epsilon-connected ordinal set

sup X is epsilon-transitive epsilon-connected ordinal set

R is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

X /\ R is Element of bool M

sup (X /\ R) is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

sup X is epsilon-transitive epsilon-connected ordinal set

R is set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

sup X is epsilon-transitive epsilon-connected ordinal set

R is epsilon-transitive epsilon-connected ordinal set

succ R is epsilon-transitive epsilon-connected ordinal non empty set

{R} is non empty trivial 1 -element set

R \/ {R} is non empty set

X1 is epsilon-transitive epsilon-connected ordinal set

RANKS is epsilon-transitive epsilon-connected ordinal set

X1 is set

R is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

sup X is epsilon-transitive epsilon-connected ordinal set

sup M is epsilon-transitive epsilon-connected ordinal set

R is epsilon-transitive epsilon-connected ordinal set

sup R is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

R is Element of bool M

R /\ X is Element of bool M

sup (R /\ X) is epsilon-transitive epsilon-connected ordinal set

bool X is non empty non finite set

X1 is Element of bool X

RANKS is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

R is epsilon-transitive epsilon-connected ordinal set

X1 is set

RANKS is epsilon-transitive epsilon-connected ordinal Element of M

R is epsilon-transitive epsilon-connected ordinal set

X1 is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

the epsilon-transitive epsilon-connected ordinal Element of M is epsilon-transitive epsilon-connected ordinal Element of M

X1 is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is epsilon-transitive epsilon-connected ordinal set

R is Element of bool M

{ b

succ X is epsilon-transitive epsilon-connected ordinal non empty set

{X} is non empty trivial 1 -element set

X \/ {X} is non empty set

X1 is epsilon-transitive epsilon-connected ordinal set

RANKS is epsilon-transitive epsilon-connected ordinal Element of M

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

R is epsilon-transitive epsilon-connected ordinal set

{ b

inf { b

{ b

inf { b

RANKS is epsilon-transitive epsilon-connected ordinal Element of M

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is epsilon-transitive epsilon-connected ordinal set

R is Element of bool M

(M,R,X) is Element of R

{ b

RANKS is set

inf { b

On { b

meet (On { b

meet { b

RANKS is epsilon-transitive epsilon-connected ordinal Element of M

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

[#] M is Element of bool M

bool M is non empty non finite set

X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

([#] M) /\ X is Element of bool M

sup (([#] M) /\ X) is epsilon-transitive epsilon-connected ordinal set

sup ([#] M) is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is epsilon-transitive epsilon-connected ordinal set

R is Element of bool M

R \ X is Element of bool M

X1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

(R \ X) /\ X1 is Element of bool M

sup ((R \ X) /\ X1) is epsilon-transitive epsilon-connected ordinal set

R /\ X1 is Element of bool M

sup (R /\ X1) is epsilon-transitive epsilon-connected ordinal set

sup X1 is epsilon-transitive epsilon-connected ordinal set

R \ X1 is Element of bool M

X1 is epsilon-transitive epsilon-connected ordinal set

RANKS is epsilon-transitive epsilon-connected ordinal set

RANKS is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

X is epsilon-transitive epsilon-connected ordinal set

M \ X is Element of bool M

bool M is non empty non finite set

[#] M is Element of bool M

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

R is Element of bool M

X1 is Element of bool M

R /\ X1 is Element of bool M

X /\ X1 is Element of bool M

RANKS is set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

X is set

R is set

bool M is non empty non finite set

RANKS1 is Element of bool M

X /\ RANKS1 is Element of bool M

X1 is Element of bool M

RANKS is Element of bool M

RANKS1 is Element of bool M

RANKS /\ RANKS1 is Element of bool M

M is set

bool M is set

bool (bool M) is set

X is Element of bool (bool M)

R is Element of X

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

R is epsilon-transitive epsilon-connected ordinal set

M \ R is Element of bool M

(M \ R) /\ X is Element of bool M

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

{ b

{ b

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is epsilon-transitive epsilon-connected ordinal set

R is epsilon-transitive epsilon-connected ordinal set

succ R is epsilon-transitive epsilon-connected ordinal non empty set

{R} is non empty trivial 1 -element set

R \/ {R} is non empty set

X1 is Element of bool M

X1 /\ X is Element of bool M

(M,X1) is Element of bool M

{ b

X /\ (M,X1) is Element of bool M

RANKS is set

RANKS1 is epsilon-transitive epsilon-connected ordinal Element of X

{ b

X1 /\ RANKS1 is Element of bool M

sup (X1 /\ RANKS1) is epsilon-transitive epsilon-connected ordinal set

N1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool N1 is non empty non finite set

X1 /\ N1 is Element of bool M

x is Element of bool N1

C is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is epsilon-transitive epsilon-connected ordinal set

succ X is epsilon-transitive epsilon-connected ordinal non empty set

{X} is non empty trivial 1 -element set

X \/ {X} is non empty set

R is Element of bool M

(M,R) is Element of bool M

{ b

R /\ M is Element of bool M

M /\ (M,R) is Element of bool M

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

(M,X) is Element of bool M

{ b

R is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

(M,X) /\ R is Element of bool M

sup ((M,X) /\ R) is epsilon-transitive epsilon-connected ordinal set

X /\ R is Element of bool M

sup (X /\ R) is epsilon-transitive epsilon-connected ordinal set

RANKS is epsilon-transitive epsilon-connected ordinal set

succ RANKS is epsilon-transitive epsilon-connected ordinal non empty set

{RANKS} is non empty trivial 1 -element set

RANKS \/ {RANKS} is non empty set

sup (succ RANKS) is epsilon-transitive epsilon-connected ordinal set

X1 is epsilon-transitive epsilon-connected ordinal Element of M

X /\ X1 is Element of bool M

sup (X /\ X1) is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

bool M is non empty non finite set

X is Element of bool M

(M,X) is Element of bool M

{ b

R is epsilon-transitive epsilon-connected ordinal set

{ (succ b

RANKS is set

RANKS1 is epsilon-transitive epsilon-connected ordinal Element of M

succ RANKS1 is epsilon-transitive epsilon-connected ordinal non empty set

{RANKS1} is non empty trivial 1 -element set

RANKS1 \/ {RANKS1} is non empty set

RANKS is Element of bool M

RANKS1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

RANKS /\ RANKS1 is Element of bool M

sup (RANKS /\ RANKS1) is epsilon-transitive epsilon-connected ordinal set

the epsilon-transitive epsilon-connected ordinal Element of RANKS1 is epsilon-transitive epsilon-connected ordinal Element of RANKS1

C is epsilon-transitive epsilon-connected ordinal set

X /\ RANKS1 is Element of bool M

sup (X /\ RANKS1) is epsilon-transitive epsilon-connected ordinal set

B5 is epsilon-transitive epsilon-connected ordinal set

succ B5 is epsilon-transitive epsilon-connected ordinal non empty set

{B5} is non empty trivial 1 -element set

B5 \/ {B5} is non empty set

succ (succ B5) is epsilon-transitive epsilon-connected ordinal non empty set

{(succ B5)} is non empty trivial 1 -element set

(succ B5) \/ {(succ B5)} is non empty set

B6 is epsilon-transitive epsilon-connected ordinal set

C3 is epsilon-transitive epsilon-connected ordinal Element of M

succ C3 is epsilon-transitive epsilon-connected ordinal non empty set

{C3} is non empty trivial 1 -element set

C3 \/ {C3} is non empty set

N1 is epsilon-transitive epsilon-connected ordinal Element of M

B5 is epsilon-transitive epsilon-connected ordinal Element of M

succ B5 is epsilon-transitive epsilon-connected ordinal non empty set

{B5} is non empty trivial 1 -element set

B5 \/ {B5} is non empty set

RANKS1 is epsilon-transitive epsilon-connected ordinal set

RANKS1 \/ R is epsilon-transitive epsilon-connected ordinal set

x is epsilon-transitive epsilon-connected ordinal set

succ x is epsilon-transitive epsilon-connected ordinal non empty set

{x} is non empty trivial 1 -element set

x \/ {x} is non empty set

sup RANKS is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

bool M is non empty non finite set

cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

X is Element of bool M

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

sup X is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

bool M is non empty non finite set

bool (bool M) is non empty non finite set

X is Element of bool (bool M)

meet X is Element of bool M

R is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

(meet X) /\ R is Element of bool M

sup ((meet X) /\ R) is epsilon-transitive epsilon-connected ordinal set

X1 is set

RANKS is (M,X)

RANKS /\ R is Element of bool M

sup (RANKS /\ R) is epsilon-transitive epsilon-connected ordinal set

sup R is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

bool M is non empty non finite set

cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

X is Element of bool M

[:NAT,X:] is set

bool [:NAT,X:] is set

R is Relation-like NAT -defined X -valued Function-like V32( NAT ,X) Element of bool [:NAT,X:]

rng R is set

sup (rng R) is epsilon-transitive epsilon-connected ordinal set

card NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

dom R is set

card (rng R) is epsilon-transitive epsilon-connected ordinal cardinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

bool M is non empty non finite set

bool (bool M) is non empty non finite set

X is non empty Element of bool (bool M)

card X is epsilon-transitive epsilon-connected ordinal non empty cardinal set

meet X is Element of bool M

R is epsilon-transitive epsilon-connected ordinal set

{ (M,b

[#] M is Element of bool M

{ (M,b

{ (M,b

{ (M,b

RANKS is epsilon-transitive epsilon-connected ordinal Element of M

{ (M,b

{ (M,b

N1 is set

x is (M,X)

(M,x,RANKS) is Element of x

RANKS is epsilon-transitive epsilon-connected ordinal Element of M

{ (M,b

{ (M,b

sup H

{ H

card { H

card H

the (M,X) is (M,X)

(M, the (M,X),RANKS) is Element of the (M,X)

N1 is epsilon-transitive epsilon-connected ordinal Element of M

RANKS is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT

RANKS1 is epsilon-transitive epsilon-connected ordinal Element of M

{ (M,b

{ (M,b

sup H

N1 is epsilon-transitive epsilon-connected ordinal Element of M

[:NAT,M:] is non empty non finite set

bool [:NAT,M:] is non empty non finite set

X1 is epsilon-transitive epsilon-connected ordinal Element of M

RANKS is Relation-like NAT -defined M -valued Function-like V32( NAT ,M) Element of bool [:NAT,M:]

RANKS . 0 is epsilon-transitive epsilon-connected ordinal Element of M

[:NAT,([#] M):] is set

bool [:NAT,([#] M):] is set

rng RANKS is set

sup (rng RANKS) is epsilon-transitive epsilon-connected ordinal set

N1 is Element of bool M

x is epsilon-transitive epsilon-connected ordinal set

dom RANKS is set

C is set

RANKS . C is set

B5 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT

B5 + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT

RANKS . (B5 + 1) is epsilon-transitive epsilon-connected ordinal Element of M

B6 is epsilon-transitive epsilon-connected ordinal set

RANKS1 is Relation-like NAT -defined [#] M -valued Function-like V32( NAT , [#] M) Element of bool [:NAT,([#] M):]

rng RANKS1 is set

sup (rng RANKS1) is epsilon-transitive epsilon-connected ordinal set

sup N1 is epsilon-transitive epsilon-connected ordinal set

x is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite Element of M

C is set

B5 is (M,X)

B5 /\ x is Element of bool M

sup (B5 /\ x) is epsilon-transitive epsilon-connected ordinal set

sup x is epsilon-transitive epsilon-connected ordinal set

B6 is epsilon-transitive epsilon-connected ordinal set

dom RANKS is set

C3 is set

RANKS . C3 is set

c

RANKS . c

(M,B5,(RANKS . c

{ (M,b

{ (M,b

LBY is epsilon-transitive epsilon-connected ordinal Element of M

sup H

c

RANKS . (c

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

bool M is non empty non finite set

cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

X is Element of bool M

(M,X) is Element of bool M

{ b

X1 is epsilon-transitive epsilon-connected ordinal set

R is non empty Element of bool M

(M,R,X1) is Element of R

RANKS1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT

N1 is Element of R

x is epsilon-transitive epsilon-connected ordinal Element of M

succ x is epsilon-transitive epsilon-connected ordinal non empty set

{x} is non empty trivial 1 -element set

x \/ {x} is non empty set

C is epsilon-transitive epsilon-connected ordinal set

B5 is Element of R

[:NAT,R:] is non empty non finite set

bool [:NAT,R:] is non empty non finite set

RANKS is Element of R

RANKS1 is Relation-like NAT -defined R -valued Function-like V32( NAT ,R) Element of bool [:NAT,R:]

RANKS1 . 0 is Element of R

dom RANKS1 is set

rng RANKS1 is set

x is epsilon-transitive epsilon-connected ordinal Element of M

sup (rng RANKS1) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

B5 is set

RANKS1 . B5 is set

B6 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT

B6 + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT

RANKS1 . (B6 + 1) is Element of R

C3 is epsilon-transitive epsilon-connected ordinal Element of M

C is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite Element of M

X /\ C is Element of bool M

sup (X /\ C) is epsilon-transitive epsilon-connected ordinal set

B5 is epsilon-transitive epsilon-connected ordinal set

B6 is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

bool M is non empty non finite set

cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

X is Element of bool M

(M,X) is Element of bool M

{ b

R is epsilon-transitive epsilon-connected ordinal set

X1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

{ b

{ b

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

{ b

X is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom X is epsilon-transitive epsilon-connected ordinal set

rng X is set

sup X is epsilon-transitive epsilon-connected ordinal set

bool M is non empty non finite set

R is Element of bool M

card R is epsilon-transitive epsilon-connected ordinal cardinal set

card (cf M) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

sup R is epsilon-transitive epsilon-connected ordinal set

(M,R) is Element of bool M

{ b

X1 is epsilon-transitive epsilon-connected ordinal set

{ (succ b

RANKS1 is Element of bool M

{ b

RANKS1 /\ { b

N1 is set

x is epsilon-transitive epsilon-connected ordinal Element of M

succ x is epsilon-transitive epsilon-connected ordinal non empty set

{x} is non empty trivial 1 -element set

x \/ {x} is non empty set

C is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M

succ (cf M) is epsilon-transitive epsilon-connected ordinal non empty set

{(cf M)} is non empty trivial 1 -element set

(cf M) \/ {(cf M)} is non empty set

(M,R) \ (succ (cf M)) is Element of bool M

{ b

((M,R) \ (succ (cf M))) /\ { b

X1 is set

RANKS is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M

bool RANKS is non empty non finite set

RANKS /\ R is Element of bool M

{ b

R /\ RANKS is Element of bool M

sup (R /\ RANKS) is epsilon-transitive epsilon-connected ordinal set

RANKS1 is Element of bool RANKS

cf RANKS is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

card RANKS1 is epsilon-transitive epsilon-connected ordinal cardinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

{ b

bool M is non empty non finite set

R is epsilon-transitive epsilon-connected ordinal cardinal set

nextcard R is epsilon-transitive epsilon-connected ordinal cardinal set

succ R is epsilon-transitive epsilon-connected ordinal non empty set

{R} is non empty trivial 1 -element set

R \/ {R} is non empty set

M \ (succ R) is Element of bool M

X is Element of bool M

X /\ (M \ (succ R)) is Element of bool M

X1 is set

RANKS is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

{ b

bool M is non empty non finite set

R is epsilon-transitive epsilon-connected ordinal cardinal set

exp (2,R) is epsilon-transitive epsilon-connected ordinal cardinal set

succ R is epsilon-transitive epsilon-connected ordinal non empty set

{R} is non empty trivial 1 -element set

R \/ {R} is non empty set

M \ (succ R) is Element of bool M

X is Element of bool M

X /\ (M \ (succ R)) is Element of bool M

X1 is set

RANKS is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

M is set

union M is set

X is set

R is set

X1 is set

RANKS is epsilon-transitive epsilon-connected ordinal cardinal set

X is epsilon-transitive epsilon-connected ordinal set

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

R is set

X1 is epsilon-transitive epsilon-connected ordinal set

RANKS is set

RANKS1 is set

N1 is epsilon-transitive epsilon-connected ordinal cardinal set

card N1 is epsilon-transitive epsilon-connected ordinal cardinal set

M is set

card M is epsilon-transitive epsilon-connected ordinal cardinal set

union M is set

card (union M) is epsilon-transitive epsilon-connected ordinal cardinal set

X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

cf X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

R is non empty set

{ H

card { H

card R is epsilon-transitive epsilon-connected ordinal non empty cardinal set

RANKS is set

RANKS1 is Element of R

card RANKS1 is epsilon-transitive epsilon-connected ordinal cardinal set

RANKS is set

union { H

RANKS1 is set

RANKS is epsilon-transitive epsilon-connected ordinal cardinal set

(card R) *` RANKS is epsilon-transitive epsilon-connected ordinal cardinal set

(cf X) *` X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

RANKS1 is set

card RANKS1 is epsilon-transitive epsilon-connected ordinal cardinal set

union R is set

card (union R) is epsilon-transitive epsilon-connected ordinal cardinal set

X *` X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

X is epsilon-transitive epsilon-connected ordinal set

Rank X is epsilon-transitive set

card (Rank X) is epsilon-transitive epsilon-connected ordinal cardinal set

R is epsilon-transitive epsilon-connected ordinal set

Rank R is epsilon-transitive set

card (Rank R) is epsilon-transitive epsilon-connected ordinal cardinal set

succ R is epsilon-transitive epsilon-connected ordinal non empty set

{R} is non empty trivial 1 -element set

R \/ {R} is non empty set

Rank (succ R) is epsilon-transitive set

card (Rank (succ R)) is epsilon-transitive epsilon-connected ordinal cardinal set

exp (2,(card (Rank R))) is epsilon-transitive epsilon-connected ordinal cardinal set

bool (Rank R) is Element of bool (bool (Rank R))

bool (Rank R) is set

bool (bool (Rank R)) is set

cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

R is epsilon-transitive epsilon-connected ordinal set

Rank R is epsilon-transitive set

card (Rank R) is epsilon-transitive epsilon-connected ordinal cardinal set

X1 is Relation-like T-Sequence-like Function-like set

dom X1 is epsilon-transitive epsilon-connected ordinal set

rng X1 is set

card (rng X1) is epsilon-transitive epsilon-connected ordinal cardinal set

card R is epsilon-transitive epsilon-connected ordinal cardinal set

RANKS is set

card RANKS is epsilon-transitive epsilon-connected ordinal cardinal set

RANKS1 is set

X1 . RANKS1 is set

N1 is epsilon-transitive epsilon-connected ordinal Element of R

Rank N1 is epsilon-transitive set

Union X1 is set

union (rng X1) is set

card (Rank {}) is epsilon-transitive epsilon-connected ordinal cardinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

Rank M is epsilon-transitive set

card (Rank M) is epsilon-transitive epsilon-connected ordinal cardinal set

X is Relation-like T-Sequence-like Function-like set

dom X is epsilon-transitive epsilon-connected ordinal set

rng X is set

R is set

X1 is set

RANKS is set

X . RANKS is set

RANKS1 is set

X . RANKS1 is set

x is epsilon-transitive epsilon-connected ordinal set

Rank x is epsilon-transitive set

N1 is epsilon-transitive epsilon-connected ordinal set

Rank N1 is epsilon-transitive set

card M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

Union X is set

union (rng X) is set

R is set

X1 is set

X . X1 is set

RANKS is epsilon-transitive epsilon-connected ordinal set

Rank RANKS is epsilon-transitive set

card (Rank RANKS) is epsilon-transitive epsilon-connected ordinal cardinal set

card R is epsilon-transitive epsilon-connected ordinal cardinal set

card (union (rng X)) is epsilon-transitive epsilon-connected ordinal cardinal set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

Rank M is epsilon-transitive set

X is set

R is set

X is set

bool X is Element of bool (bool X)

bool X is set

bool (bool X) is set

R is epsilon-transitive epsilon-connected ordinal set

Rank R is epsilon-transitive set

succ R is epsilon-transitive epsilon-connected ordinal non empty set

{R} is non empty trivial 1 -element set

R \/ {R} is non empty set

Rank (succ R) is epsilon-transitive set

cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set

X is set

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

the_rank_of X is epsilon-transitive epsilon-connected ordinal set

card (Rank M) is epsilon-transitive epsilon-connected ordinal cardinal set

X1 is non empty set

{ H

RANKS1 is set

RANKS1 is set

N1 is Element of X1

the_rank_of N1 is epsilon-transitive epsilon-connected ordinal set

bool M is non empty non finite set

N1 is epsilon-transitive epsilon-connected ordinal set

x is set

the_rank_of x is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

RANKS1 is Element of bool M

card RANKS1 is epsilon-transitive epsilon-connected ordinal cardinal set

card { H

card X1 is epsilon-transitive epsilon-connected ordinal non empty cardinal set

N1 is epsilon-transitive epsilon-connected ordinal set

N1 is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal non empty set

Rank M is epsilon-transitive set

M is epsilon-transitive epsilon-connected ordinal non empty set

Rank M is epsilon-transitive set

M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set

Rank M is epsilon-transitive non empty set