:: CARD_LAR semantic presentation

REAL is set

bool NAT is non empty non finite set

dom {} is set
rng {} is set

bool M is non empty non finite set

bool M is non empty non finite set

bool M is non empty non finite set
X is Element of bool M

X /\ R is Element of bool M

X /\ R is Element of bool M

bool M is non empty non finite set
X is Element of bool M

R is set

bool M is non empty non finite set
X is Element of bool M

{R} is non empty trivial 1 -element set
R \/ {R} is non empty set

X1 is set

bool M is non empty non finite set
X is Element of bool M

bool M is non empty non finite set

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

bool X is non empty non finite set
X1 is Element of bool X

bool M is non empty non finite set
X is Element of bool M

X1 is set

bool M is non empty non finite set
X is Element of bool M

bool M is non empty non finite set

R is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( b1 in R & X in b1 ) } is set

{X} is non empty trivial 1 -element set
X \/ {X} is non empty set

bool M is non empty non finite set
X is Element of bool M

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( b1 in X & R in b1 ) } is set
inf { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( b1 in X & R in b1 ) } is epsilon-transitive epsilon-connected ordinal set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
inf { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is epsilon-transitive epsilon-connected ordinal set

bool M is non empty non finite set

R is Element of bool M
(M,R,X) is Element of R
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
RANKS is set
inf { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is epsilon-transitive epsilon-connected ordinal set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
meet (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } ) is set
meet { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set

[#] M is Element of bool M
bool M is non empty non finite set

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

bool M is non empty non finite set

R is Element of bool M
R \ X is Element of bool M

(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

R \ X1 is Element of bool M

M \ X is Element of bool M
bool M is non empty non finite set
[#] M is Element of bool M

bool M is 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

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

bool M is non empty non finite set
X is Element of bool M

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

bool M is non empty non finite set
X is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X /\ b1) = b1 ) } is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set

bool M is non empty non finite 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
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X1 /\ b1) = b1 ) } is set
X /\ (M,X1) is Element of bool M
RANKS is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
X1 /\ RANKS1 is Element of bool M
sup (X1 /\ RANKS1) is epsilon-transitive epsilon-connected ordinal set

bool N1 is non empty non finite set
X1 /\ N1 is Element of bool M
x is Element of bool N1

bool M is non empty non finite 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
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (R /\ b1) = b1 ) } is set
R /\ M is Element of bool M
M /\ (M,R) is Element of bool M

bool M is non empty non finite set
X is Element of bool M
(M,X) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X /\ b1) = b1 ) } is set

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

X /\ R is Element of bool M

{RANKS} is non empty trivial 1 -element set
RANKS \/ {RANKS} is non empty set

X /\ X1 is Element of bool M

bool M is non empty non finite set
X is Element of bool M
(M,X) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X /\ b1) = b1 ) } is set

{ (succ b1) where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( b1 in X & R in succ b1 ) } is set
RANKS is set

{RANKS1} is non empty trivial 1 -element set
RANKS1 \/ {RANKS1} is non empty set
RANKS is Element of bool M

RANKS /\ RANKS1 is Element of bool M
sup (RANKS /\ RANKS1) 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 non empty trivial 1 -element set
B5 \/ {B5} is non empty set

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

{C3} is non empty trivial 1 -element set
C3 \/ {C3} is non empty set

{B5} is non empty trivial 1 -element set
B5 \/ {B5} is non empty set

{x} is non empty trivial 1 -element set
x \/ {x} is non empty set

bool M is non empty non finite set

X is Element of bool M

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

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

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

bool M is non empty non finite set

X is Element of bool M
[:NAT,X:] is set
bool [:NAT,X:] is set

rng R is set

dom R is 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)

meet X is Element of bool M

{ (M,b1,a1) where b1 is (M,X) : b1 in X } is set
[#] M is Element of bool M
{ (M,b1,a1) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M
{ (M,b1,a2) where b1 is (M,X) : b1 in X } is set
{ (M,b1,a2) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M

{ (M,b1,RANKS) where b1 is (M,X) : b1 in X } is set
{ (M,b1,RANKS) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M
N1 is set
x is (M,X)
(M,x,RANKS) is Element of x

{ (M,b1,RANKS) where b1 is (M,X) : b1 in X } is set
{ (M,b1,RANKS) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M
sup H1(RANKS) is epsilon-transitive epsilon-connected ordinal set
{ H2(b1) where b1 is (M,X) : b1 in X } is set
card { H2(b1) where b1 is (M,X) : b1 in X } is epsilon-transitive epsilon-connected ordinal cardinal set

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

{ (M,b1,RANKS1) where b1 is (M,X) : b1 in X } is set
{ (M,b1,RANKS1) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M
sup H1(RANKS1) is epsilon-transitive epsilon-connected ordinal set

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

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

N1 is Element of bool M

dom RANKS is set
C is set
RANKS . C is set

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

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

C is set
B5 is (M,X)
B5 /\ x is Element of bool M

dom RANKS is set
C3 is set
RANKS . C3 is set

RANKS . c13 is epsilon-transitive epsilon-connected ordinal Element of M
(M,B5,(RANKS . c13)) is Element of B5
{ (M,b1,(RANKS . c13)) where b1 is (M,X) : b1 in X } is set
{ (M,b1,(RANKS . c13)) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M

sup H1(RANKS . c13) is epsilon-transitive epsilon-connected ordinal set

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

bool M is non empty non finite set

X is Element of bool M
(M,X) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X /\ b1) = b1 ) } is set

R is non empty Element of bool M
(M,R,X1) is Element of R

N1 is Element of R

{x} is non empty trivial 1 -element set
x \/ {x} is non empty 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

B5 is set
RANKS1 . B5 is set

RANKS1 . (B6 + 1) is Element of R

X /\ C is Element of bool M

bool M is non empty non finite set

X is Element of bool M
(M,X) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X /\ b1) = b1 ) } is set

{ } is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } is set

rng X is set

bool M is non empty non finite set
R is Element of bool M

(M,R) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (R /\ b1) = b1 ) } is set

{ (succ b1) where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( b1 in R & X1 in succ b1 ) } is set
RANKS1 is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } /\ RANKS1 is Element of bool M
RANKS1 /\ { b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } is Element of bool M
N1 is set

{x} is non empty trivial 1 -element set
x \/ {x} is 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
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } /\ ((M,R) \ (succ (cf M))) is Element of bool M
((M,R) \ (succ (cf M))) /\ { b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } is Element of bool M
X1 is set

bool RANKS is non empty non finite set
RANKS /\ R is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
R /\ RANKS is Element of bool M

RANKS1 is Element of bool RANKS

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } is set
bool M is non empty non finite 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

{ } is set
bool M is non empty non finite 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

M is set
union M is set
X is set
R is set
X1 is set

R is set

RANKS is set
RANKS1 is set

M is set

union M is set

R is non empty set
{ H1(b1) where b1 is Element of R : b1 in R } is set
card { H1(b1) where b1 is Element of R : b1 in R } is epsilon-transitive epsilon-connected ordinal cardinal set

RANKS is set
RANKS1 is Element of R

RANKS is set
union { H1(b1) where b1 is Element of R : b1 in R } is set
RANKS1 is set

RANKS1 is set

union R is set

{R} is non empty trivial 1 -element set
R \/ {R} is non empty set

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

rng X1 is set

RANKS is set

RANKS1 is set
X1 . RANKS1 is set

Union X1 is set
union (rng X1) is 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

Union X is set
union (rng X) is set
R is set
X1 is set
X . X1 is set

Rank RANKS 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 non empty trivial 1 -element set
R \/ {R} is non empty set

X is set

X1 is non empty set
{ H2(b1) where b1 is Element of X1 : b1 in X1 } is set
RANKS1 is set
RANKS1 is set
N1 is Element of X1

bool M is non empty non finite set

x is set

RANKS1 is Element of bool M

card { H2(b1) where b1 is Element of X1 : b1 in X1 } is epsilon-transitive epsilon-connected ordinal cardinal set