:: KNASTER semantic presentation

REAL is set

NAT is epsilon-transitive epsilon-connected ordinal non empty V50() cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

NAT is epsilon-transitive epsilon-connected ordinal non empty V50() cardinal limit_cardinal set

bool NAT is non empty V50() set

bool NAT is non empty V50() set

{} is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V50() cardinal {} -element set

the Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V50() cardinal {} -element set is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V50() cardinal {} -element set

1 is epsilon-transitive epsilon-connected ordinal natural non empty V50() cardinal Element of NAT

0 is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V50() cardinal {} -element Element of NAT

A is Relation-like Function-like set

f is Relation-like Function-like set

dom f is set

rng f is set

gf is Relation-like Function-like set

f \/ gf is set

dom gf is set

rng gf is set

dom A is set

(dom f) \/ (dom gf) is set

g is set

gg is set

f . g is set

f . gg is set

[gg,(f . gg)] is set

{gg,(f . gg)} is non empty set

{gg} is non empty trivial 1 -element set

{{gg,(f . gg)},{gg}} is non empty set

A . gg is set

[g,(f . g)] is set

{g,(f . g)} is non empty set

{g} is non empty trivial 1 -element set

{{g,(f . g)},{g}} is non empty set

A . g is set

g is set

gg is set

gf . g is set

gf . gg is set

[gg,(gf . gg)] is set

{gg,(gf . gg)} is non empty set

{gg} is non empty trivial 1 -element set

{{gg,(gf . gg)},{gg}} is non empty set

A . gg is set

[g,(gf . g)] is set

{g,(gf . g)} is non empty set

{g} is non empty trivial 1 -element set

{{g,(gf . g)},{g}} is non empty set

A . g is set

g is set

gg is set

f . gg is set

c

gf . c

[c

{c

{c

{{c

A . c

[gg,g] is set

{gg,g} is non empty set

{gg} is non empty trivial 1 -element set

{{gg,g},{gg}} is non empty set

A . gg is set

f +* gf is Relation-like Function-like set

A is set

[:A,A:] is set

bool [:A,A:] is non empty set

f is set

gf is epsilon-transitive epsilon-connected ordinal natural V50() cardinal Element of NAT

g is Relation-like A -defined A -valued Function-like quasi_total Element of bool [:A,A:]

iter (g,gf) is Relation-like A -defined A -valued Function-like quasi_total Element of bool [:A,A:]

g . f is set

dom (iter (g,gf)) is Element of bool A

bool A is non empty set

dom g is Element of bool A

rng g is Element of bool A

(iter (g,gf)) . (g . f) is set

(iter (g,gf)) . f is set

g * (iter (g,gf)) is Relation-like A -defined A -valued Function-like Element of bool [:A,A:]

(g * (iter (g,gf))) . f is set

gf + 1 is epsilon-transitive epsilon-connected ordinal natural V50() cardinal Element of NAT

iter (g,(gf + 1)) is Relation-like A -defined A -valued Function-like quasi_total Element of bool [:A,A:]

(iter (g,(gf + 1))) . f is set

(iter (g,gf)) * g is Relation-like A -defined A -valued Function-like Element of bool [:A,A:]

((iter (g,gf)) * g) . f is set

A is set

[:A,A:] is set

bool [:A,A:] is non empty set

f is set

gf is Relation-like A -defined A -valued Function-like quasi_total Element of bool [:A,A:]

g is epsilon-transitive epsilon-connected ordinal natural V50() cardinal Element of NAT

iter (gf,g) is Relation-like A -defined A -valued Function-like quasi_total Element of bool [:A,A:]

dom gf is Element of bool A

bool A is non empty set

dom (iter (gf,g)) is Element of bool A

gf . f is set

A is non empty set

f is non empty set

[:A,f:] is non empty set

bool [:A,f:] is non empty set

gf is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]

dom gf is Element of bool A

bool A is non empty set

g is Element of A

gg is Element of A

gf . g is Element of f

gf . gg is Element of f

g is set

dom gf is set

gg is set

gf . g is set

gf . gg is set

A is set

f is non empty set

[:A,f:] is set

bool [:A,f:] is non empty set

the Element of f is Element of f

A --> the Element of f is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]

g is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]

gg is set

dom g is set

c

g . gg is set

g . c

dom g is Element of bool A

bool A is non empty set

A is set

bool A is non empty Element of bool (bool A)

bool A is non empty set

bool (bool A) is non empty set

[:(bool A),(bool A):] is non empty set

bool [:(bool A),(bool A):] is non empty set

f is Relation-like bool A -defined bool A -valued Function-like quasi_total c=-monotone Element of bool [:(bool A),(bool A):]

{ b

meet { b

{ b

gf is Element of bool (bool A)

g is Element of bool (bool A)

meet g is Element of bool A

{ b

union { b

{ b

gf is Element of bool (bool A)

union gf is Element of bool A

A is set

bool A is non empty Element of bool (bool A)

bool A is non empty set

bool (bool A) is non empty set

[:(bool A),(bool A):] is non empty set

bool [:(bool A),(bool A):] is non empty set

f is Relation-like bool A -defined bool A -valued Function-like quasi_total c=-monotone Element of bool [:(bool A),(bool A):]

(A,f) is Element of bool A

{ b

meet { b

{ b

gf is Element of bool (bool A)

g is Element of bool (bool A)

meet g is Element of bool A

c

f . c

C is set

C is Element of bool A

f . C is Element of bool A

f . (meet g) is Element of bool A

f . (f . (meet g)) is Element of bool A

f . (A,f) is Element of bool A

A is set

bool A is non empty Element of bool (bool A)

bool A is non empty set

bool (bool A) is non empty set

[:(bool A),(bool A):] is non empty set

bool [:(bool A),(bool A):] is non empty set

f is Relation-like bool A -defined bool A -valued Function-like quasi_total c=-monotone Element of bool [:(bool A),(bool A):]

(A,f) is Element of bool A

{ b

union { b

{ b

gf is Element of bool (bool A)

union gf is Element of bool A

gg is set

c

f . c

f . (union gf) is Element of bool A

f . (f . (union gf)) is Element of bool A

f . (A,f) is Element of bool A

A is set

bool A is non empty Element of bool (bool A)

bool A is non empty set

bool (bool A) is non empty set

[:(bool A),(bool A):] is non empty set

bool [:(bool A),(bool A):] is non empty set

f is Relation-like bool A -defined bool A -valued Function-like quasi_total c=-monotone Element of bool [:(bool A),(bool A):]

(A,f) is Element of bool A

{ b

meet { b

gf is Element of bool A

f . gf is Element of bool A

A is set

bool A is non empty Element of bool (bool A)

bool A is non empty set

bool (bool A) is non empty set

[:(bool A),(bool A):] is non empty set

bool [:(bool A),(bool A):] is non empty set

f is Relation-like bool A -defined bool A -valued Function-like quasi_total c=-monotone Element of bool [:(bool A),(bool A):]

(A,f) is Element of bool A

{ b

union { b

gf is Element of bool A

f . gf is Element of bool A

A is set

bool A is non empty Element of bool (bool A)

bool A is non empty set

bool (bool A) is non empty set

[:(bool A),(bool A):] is non empty set

bool [:(bool A),(bool A):] is non empty set

f is Relation-like bool A -defined bool A -valued Function-like quasi_total c=-monotone Element of bool [:(bool A),(bool A):]

(A,f) is Element of bool A

{ b

meet { b

(A,f) is Element of bool A

{ b

union { b

gf is Element of bool A

f . gf is Element of bool A

F

F

bool F

bool F

bool (bool F

A is Relation-like Function-like set

dom A is set

rng A is set

f is set

gf is set

A . gf is set

F

[:(bool F

bool [:(bool F

gf is set

f is Relation-like bool F

dom f is Element of bool (bool F

bool (bool F

g is set

f . gf is set

F

f . g is set

F

gf is Relation-like bool F

(F

{ b

meet { b

g is Element of bool F

F

gf . g is Element of bool F

A is non empty set

f is non empty set

[:A,f:] is non empty set

bool [:A,f:] is non empty set

[:f,A:] is non empty set

bool [:f,A:] is non empty set

gf is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]

g is Relation-like f -defined A -valued Function-like quasi_total Element of bool [:f,A:]

bool A is non empty set

bool A is non empty Element of bool (bool A)

bool (bool A) is non empty set

gg is set

gf .: gg is Element of bool f

bool f is non empty set

f \ (gf .: gg) is Element of bool f

g .: (f \ (gf .: gg)) is Element of bool A

A \ (g .: (f \ (gf .: gg))) is Element of bool A

[:(bool A),(bool A):] is non empty set

bool [:(bool A),(bool A):] is non empty set

gg is Relation-like bool A -defined bool A -valued Function-like quasi_total Element of bool [:(bool A),(bool A):]

c

dom gg is Element of bool (bool A)

bool (bool A) is non empty set

C is set

gf .: c

bool f is non empty set

gf .: C is Element of bool f

f \ (gf .: C) is Element of bool f

f \ (gf .: c

g .: (f \ (gf .: C)) is Element of bool A

g .: (f \ (gf .: c

A \ (g .: (f \ (gf .: c

A \ (g .: (f \ (gf .: C))) is Element of bool A

gg . c

gg . C is set

c

(A,c

{ b

meet { b

C is Element of bool A

gf .: C is Element of bool f

A \ C is Element of bool A

C is Element of bool A

C \/ C is set

O is Element of bool f

f \ O is Element of bool f

p9 is Element of bool f

O \/ p9 is set

g .: p9 is Element of bool A

C \/ C is Element of bool A

O \/ p9 is Element of bool f

f \ (gf .: C) is Element of bool f

g .: (f \ (gf .: C)) is Element of bool A

A /\ (g .: (f \ (gf .: C))) is Element of bool A

A \ (g .: (f \ (gf .: C))) is Element of bool A

A \ (A \ (g .: (f \ (gf .: C)))) is Element of bool A

c

A \ (c

A is non empty set

f is non empty set

[:A,f:] is non empty set

bool [:A,f:] is non empty set

[:f,A:] is non empty set

bool [:f,A:] is non empty set

gf is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]

g is Relation-like f -defined A -valued Function-like quasi_total Element of bool [:f,A:]

gg is set

c

C is set

C is set

gg \/ c

C \/ C is set

gf .: gg is Element of bool f

bool f is non empty set

g .: C is Element of bool A

bool A is non empty set

g | C is Relation-like f -defined A -valued Function-like Element of bool [:f,A:]

gf | gg is Relation-like A -defined f -valued Function-like Element of bool [:A,f:]

dom gf is Element of bool A

dom (gf | gg) is Element of bool A

(g | C) " is Relation-like Function-like set

(gf | gg) +* ((g | C) ") is Relation-like Function-like set

rng (g | C) is Element of bool A

dom ((g | C) ") is set

dom ((gf | gg) +* ((g | C) ")) is set

rng (gf | gg) is Element of bool f

dom g is Element of bool f

dom (g | C) is Element of bool f

rng ((g | C) ") is set

(gf | gg) \/ ((g | C) ") is set

rng ((gf | gg) +* ((g | C) ")) is set

r is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]

A is non empty set

f is non empty set

[:A,f:] is non empty set

bool [:A,f:] is non empty set

gf is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]

g is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]

rng g is Element of bool f

bool f is non empty set

gg is set

g . gg is set

c

dom g is Element of bool A

bool A is non empty set

[gg,c

{gg,c

{gg} is non empty trivial 1 -element set

{{gg,c

gg is set

c

g . c

C is set

[C,gg] is set

{C,gg} is non empty set

{C} is non empty trivial 1 -element set

{{C,gg},{C}} is non empty set

gg is set

c

[gg,c

{gg,c

{gg} is non empty trivial 1 -element set

{{gg,c

C is set

C is set

[C,C] is set

{C,C} is non empty set

{C} is non empty trivial 1 -element set

{{C,C},{C}} is non empty set

g . C is set

g . gg is set

A is non empty set

f is non empty set

[:A,f:] is non empty set

bool [:A,f:] is non empty set

[:f,A:] is non empty set

bool [:f,A:] is non empty set

gf is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]

g is Relation-like f -defined A -valued Function-like quasi_total Element of bool [:f,A:]

gg is Relation-like A -defined f -valued Function-like quasi_total Element of bool [:A,f:]

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

g is epsilon-transitive epsilon-connected ordinal set

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

gf is Element of the carrier of A

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of A:]

gg is set

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

last C is set

dom C is epsilon-transitive epsilon-connected ordinal set

C . {} is set

rng C is set

c

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

last C is set

dom C is epsilon-transitive epsilon-connected ordinal set

C . {} is set

rng C is set

O is set

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

last p9 is set

dom p9 is epsilon-transitive epsilon-connected ordinal set

p9 . {} is set

gg is set

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

last C is set

dom C is epsilon-transitive epsilon-connected ordinal set

C . {} is set

rng C is set

c

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

last C is set

dom C is epsilon-transitive epsilon-connected ordinal set

C . {} is set

rng C is set

O is set

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

last p9 is set

dom p9 is epsilon-transitive epsilon-connected ordinal set

p9 . {} is set

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

(A,f,gf,{}) is set

gg is set

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is set

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

C is set

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

last C is set

dom C is epsilon-transitive epsilon-connected ordinal set

c

succ c

C . {} is set

(A,f,gf,c

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

(A,f,gf,{}) is set

gg is set

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is set

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

C is set

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

last C is set

dom C is epsilon-transitive epsilon-connected ordinal set

c

succ c

C . {} is set

(A,f,gf,c

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

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

(A,f,gf,(succ g)) is set

(A,f,gf,g) is set

f . (A,f,gf,g) is set

c

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is set

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

C is set

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

last O is set

dom O is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

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

O . {} is set

(A,f,gf,C) is set

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

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

(A,f,gf,(succ g)) is set

(A,f,gf,g) is set

f . (A,f,gf,g) is set

c

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is set

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

C is set

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

last O is set

dom O is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

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

O . {} is set

(A,f,gf,C) is set

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is set

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

dom gg is epsilon-transitive epsilon-connected ordinal set

rng gg is set

"\/" ((rng gg),A) is Element of the carrier of A

C is set

c

(A,f,gf,c

succ c

O is set

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

last p9 is set

dom p9 is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

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

p9 . {} is set

(A,f,gf,C) is set

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is set

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

dom gg is epsilon-transitive epsilon-connected ordinal set

rng gg is set

"/\" ((rng gg),A) is Element of the carrier of A

{ b

"\/" ( { b

C is set

c

(A,f,gf,c

succ c

O is set

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

last p9 is set

dom p9 is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

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

p9 . {} is set

(A,f,gf,C) is set

A is epsilon-transitive epsilon-connected ordinal natural V50() cardinal Element of NAT

f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of f is non empty set

[: the carrier of f, the carrier of f:] is non empty set

bool [: the carrier of f, the carrier of f:] is non empty set

gf is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of f, the carrier of f:]

iter (gf,A) is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of f, the carrier of f:]

g is Element of the carrier of f

(iter (gf,A)) . g is Element of the carrier of f

(f,gf,g,A) is set

dom gf is Element of bool the carrier of f

bool the carrier of f is non empty set

field gf is set

dom gf is set

rng gf is set

(dom gf) \/ (rng gf) is set

gg is epsilon-transitive epsilon-connected ordinal natural V50() cardinal Element of NAT

iter (gf,gg) is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of f, the carrier of f:]

(iter (gf,gg)) . g is Element of the carrier of f

(f,gf,g,gg) is set

rng gf is Element of bool the carrier of f

dom (iter (gf,gg)) is Element of bool the carrier of f

gg + 1 is epsilon-transitive epsilon-connected ordinal natural V50() cardinal Element of NAT

iter (gf,(gg + 1)) is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of f, the carrier of f:]

(iter (gf,(gg + 1))) . g is Element of the carrier of f

gf * (iter (gf,gg)) is Relation-like the carrier of f -defined the carrier of f -valued Function-like Element of bool [: the carrier of f, the carrier of f:]

(gf * (iter (gf,gg))) . g is set

gf . (f,gf,g,gg) is set

succ gg is epsilon-transitive epsilon-connected ordinal natural non empty V50() cardinal set

(f,gf,g,(succ gg)) is set

(f,gf,g,(gg + 1)) is set

iter (gf,0) is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of f, the carrier of f:]

(iter (gf,0)) . g is Element of the carrier of f

id (field gf) is Relation-like field gf -defined field gf -valued Function-like one-to-one V23( field gf) Element of bool [:(field gf),(field gf):]

[:(field gf),(field gf):] is set

bool [:(field gf),(field gf):] is non empty set

(id (field gf)) . g is set

(f,gf,g,0) is set

A is epsilon-transitive epsilon-connected ordinal natural V50() cardinal Element of NAT

f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of f is non empty set

[: the carrier of f, the carrier of f:] is non empty set

bool [: the carrier of f, the carrier of f:] is non empty set

gf is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of f, the carrier of f:]

iter (gf,A) is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of f, the carrier of f:]

g is Element of the carrier of f

(iter (gf,A)) . g is Element of the carrier of f

(f,gf,g,A) is set

dom gf is Element of bool the carrier of f

bool the carrier of f is non empty set

field gf is set

dom gf is set

rng gf is set

(dom gf) \/ (rng gf) is set

gg is epsilon-transitive epsilon-connected ordinal natural V50() cardinal Element of NAT

iter (gf,gg) is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of f, the carrier of f:]

(iter (gf,gg)) . g is Element of the carrier of f

(f,gf,g,gg) is set

rng gf is Element of bool the carrier of f

dom (iter (gf,gg)) is Element of bool the carrier of f

gg + 1 is epsilon-transitive epsilon-connected ordinal natural V50() cardinal Element of NAT

iter (gf,(gg + 1)) is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of f, the carrier of f:]

(iter (gf,(gg + 1))) . g is Element of the carrier of f

gf * (iter (gf,gg)) is Relation-like the carrier of f -defined the carrier of f -valued Function-like Element of bool [: the carrier of f, the carrier of f:]

(gf * (iter (gf,gg))) . g is set

gf . (f,gf,g,gg) is set

succ gg is epsilon-transitive epsilon-connected ordinal natural non empty V50() cardinal set

(f,gf,g,(succ gg)) is set

(f,gf,g,(gg + 1)) is set

iter (gf,0) is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of bool [: the carrier of f, the carrier of f:]

(iter (gf,0)) . g is Element of the carrier of f

id (field gf) is Relation-like field gf -defined field gf -valued Function-like one-to-one V23( field gf) Element of bool [:(field gf),(field gf):]

[:(field gf),(field gf):] is set

bool [:(field gf),(field gf):] is non empty set

(id (field gf)) . g is set

(f,gf,g,0) is set

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is set

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is set

c

f . c

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

(A,f,gf,(succ gg)) is set

gg is epsilon-transitive epsilon-connected ordinal set

c

dom c

(A,f,gf,gg) is set

rng c

"\/" ((rng c

(A,f,gf,{}) is set

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is set

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is set

c

f . c

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

(A,f,gf,(succ gg)) is set

gg is epsilon-transitive epsilon-connected ordinal set

c

dom c

(A,f,gf,gg) is set

rng c

"/\" ((rng c

{ b

"\/" ( { b

(A,f,gf,{}) is set

A is non empty LattStr

the carrier of A is non empty set

bool the carrier of A is non empty set

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of A is non empty set

bool the carrier of A is non empty set

f is Element of bool the carrier of A

gf is Element of the carrier of A

g is Element of the carrier of A

gf "\/" g is Element of the carrier of A

gg is Element of the carrier of A

c

gf is Element of the carrier of A

g is Element of the carrier of A

gf "/\" g is Element of the carrier of A

gg is Element of the carrier of A

c

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of A is non empty set

bool the carrier of A is non empty set

f is non empty (A) (A) Element of bool the carrier of A

LattRel A is Relation-like the carrier of A -defined the carrier of A -valued V23( the carrier of A) reflexive antisymmetric transitive Element of bool [: the carrier of A, the carrier of A:]

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

(LattRel A) |_2 f is Relation-like set

[:f,f:] is non empty set

(LattRel A) /\ [:f,f:] is set

bool [:f,f:] is non empty set

field (LattRel A) is set

dom (LattRel A) is set

rng (LattRel A) is set

(dom (LattRel A)) \/ (rng (LattRel A)) is set

c

field c

dom c

rng c

(dom c

C is set

[C,C] is set

{C,C} is non empty set

{C} is non empty trivial 1 -element set

{{C,C},{C}} is non empty set

dom c

bool f is non empty set

C is Relation-like f -defined f -valued V23(f) reflexive antisymmetric transitive Element of bool [:f,f:]

RelStr(# f,C #) is strict RelStr

latt RelStr(# f,C #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

O is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of O is non empty set

the carrier of RelStr(# f,C #) is set

p9 is Element of the carrier of RelStr(# f,C #)

p is Element of the carrier of RelStr(# f,C #)

r is Element of the carrier of A

r99 is Element of the carrier of A

r9 is Element of the carrier of A

[r99,r9] is set

{r99,r9} is non empty set

{r99} is non empty trivial 1 -element set

{{r99,r9},{r99}} is non empty set

q is Element of the carrier of RelStr(# f,C #)

[r,r9] is set

{r,r9} is non empty set

{r} is non empty trivial 1 -element set

{{r,r9},{r}} is non empty set

q99 is Element of the carrier of RelStr(# f,C #)

[p,q99] is set

{p,q99} is non empty set

{p} is non empty trivial 1 -element set

{{p,q99},{p}} is non empty set

z9L is Element of the carrier of A

[p9,q99] is set

{p9,q99} is non empty set

{p9} is non empty trivial 1 -element set

{{p9,q99},{p9}} is non empty set

[r9,z9L] is set

{r9,z9L} is non empty set

{r9} is non empty trivial 1 -element set

{{r9,z9L},{r9}} is non empty set

the carrier of RelStr(# f,C #) is set

p9 is Element of the carrier of RelStr(# f,C #)

p is Element of the carrier of RelStr(# f,C #)

r is Element of the carrier of A

r99 is Element of the carrier of A

r9 is Element of the carrier of A

[r9,r99] is set

{r9,r99} is non empty set

{r9} is non empty trivial 1 -element set

{{r9,r99},{r9}} is non empty set

q is Element of the carrier of RelStr(# f,C #)

[r9,r] is set

{r9,r} is non empty set

{{r9,r},{r9}} is non empty set

q99 is Element of the carrier of RelStr(# f,C #)

[q99,p] is set

{q99,p} is non empty set

{q99} is non empty trivial 1 -element set

{{q99,p},{q99}} is non empty set

z9L is Element of the carrier of A

[q99,p9] is set

{q99,p9} is non empty set

{{q99,p9},{q99}} is non empty set

[z9L,r9] is set

{z9L,r9} is non empty set

{z9L} is non empty trivial 1 -element set

{{z9L,r9},{z9L}} is non empty set

LattPOSet O is non empty strict reflexive transitive antisymmetric RelStr

LattRel O is Relation-like the carrier of O -defined the carrier of O -valued V23( the carrier of O) reflexive antisymmetric transitive Element of bool [: the carrier of O, the carrier of O:]

[: the carrier of O, the carrier of O:] is non empty set

bool [: the carrier of O, the carrier of O:] is non empty set

RelStr(# the carrier of O,(LattRel O) #) is strict RelStr

p9 is Element of the carrier of O

p is Element of the carrier of O

r is Element of the carrier of A

r99 is Element of the carrier of A

[p9,p] is set

{p9,p} is non empty set

{p9} is non empty trivial 1 -element set

{{p9,p},{p9}} is non empty set

gf is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of gf is non empty set

g is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of g is non empty set

LattRel g is Relation-like the carrier of g -defined the carrier of g -valued V23( the carrier of g) reflexive antisymmetric transitive Element of bool [: the carrier of g, the carrier of g:]

[: the carrier of g, the carrier of g:] is non empty set

bool [: the carrier of g, the carrier of g:] is non empty set

{ [b

LattRel gf is Relation-like the carrier of gf -defined the carrier of gf -valued V23( the carrier of gf) reflexive antisymmetric transitive Element of bool [: the carrier of gf, the carrier of gf:]

[: the carrier of gf, the carrier of gf:] is non empty set

bool [: the carrier of gf, the carrier of gf:] is non empty set

{ [b

gg is set

c

C is Element of the carrier of gf

[c

{c

{c

{{c

C is Element of the carrier of gf

O is Element of the carrier of gf

p9 is Element of the carrier of g

p is Element of the carrier of g

r is Element of the carrier of A

r99 is Element of the carrier of A

r9 is Element of the carrier of A

q is Element of the carrier of A

c

C is Element of the carrier of g

[c

{c

{c

{{c

C is Element of the carrier of g

O is Element of the carrier of g

p9 is Element of the carrier of gf

p is Element of the carrier of gf

r is Element of the carrier of A

r99 is Element of the carrier of A

r9 is Element of the carrier of A

q is Element of the carrier of A

LattPOSet gf is non empty strict reflexive transitive antisymmetric RelStr

RelStr(# the carrier of gf,(LattRel gf) #) is strict RelStr

LattPOSet g is non empty strict reflexive transitive antisymmetric RelStr

RelStr(# the carrier of g,(LattRel g) #) is strict RelStr

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

{ b

{ (f . b

"\/" ( { b

"\/" ( { (f . b

C is Element of the carrier of A

C is Element of the carrier of A

f . C is Element of the carrier of A

f . ("\/" ( { b

C is Element of the carrier of A

C is Element of the carrier of A

f . C is Element of the carrier of A

O is Element of the carrier of A

p9 is Element of the carrier of A

f . (f . ("\/" ( { b

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

f . gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

gg is set

c

(A,f,gf,c

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

dom C is epsilon-transitive epsilon-connected ordinal set

C . c

rng C is set

"\/" ((rng C),A) is Element of the carrier of A

(A,f,gf,g) is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is Element of the carrier of A

f . (A,f,gf,g) is Element of the carrier of A

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

(A,f,gf,(succ g)) is Element of the carrier of A

(A,f,gf,{}) is Element of the carrier of A

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

f . gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

gg is set

c

(A,f,gf,c

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

dom C is epsilon-transitive epsilon-connected ordinal set

C . c

rng C is set

"/\" ((rng C),A) is Element of the carrier of A

{ b

"\/" ( { b

(A,f,gf,g) is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is Element of the carrier of A

f . (A,f,gf,g) is Element of the carrier of A

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

(A,f,gf,(succ g)) is Element of the carrier of A

(A,f,gf,{}) is Element of the carrier of A

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

f . gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is Element of the carrier of A

c

(A,f,gf,c

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

dom C is epsilon-transitive epsilon-connected ordinal set

C . gg is set

rng C is set

"\/" ((rng C),A) is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

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

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is Element of the carrier of A

c

(A,f,gf,c

(A,f,gf,g) is Element of the carrier of A

(A,f,gf,(succ g)) is Element of the carrier of A

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

dom C is epsilon-transitive epsilon-connected ordinal set

rng C is set

C is Element of the carrier of A

O is set

C . O is set

p9 is epsilon-transitive epsilon-connected ordinal set

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

(A,f,gf,p9) is Element of the carrier of A

f . (A,f,gf,p9) is Element of the carrier of A

f . (A,f,gf,g) is Element of the carrier of A

(A,f,gf,(succ p9)) is Element of the carrier of A

"\/" ((rng C),A) is Element of the carrier of A

C is epsilon-transitive epsilon-connected ordinal set

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

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty trivial 1 -element set

C \/ {C} is non empty set

(A,f,gf,C) is Element of the carrier of A

f . (A,f,gf,C) is Element of the carrier of A

f . (A,f,gf,g) is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is Element of the carrier of A

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is Element of the carrier of A

c

C is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,c

(A,f,gf,C) is Element of the carrier of A

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

f . gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is Element of the carrier of A

c

(A,f,gf,c

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

dom C is epsilon-transitive epsilon-connected ordinal set

C . gg is set

rng C is set

"/\" ((rng C),A) is Element of the carrier of A

{ b

"\/" ( { b

g is epsilon-transitive epsilon-connected ordinal set

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

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is Element of the carrier of A

c

(A,f,gf,c

(A,f,gf,(succ g)) is Element of the carrier of A

(A,f,gf,g) is Element of the carrier of A

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

dom C is epsilon-transitive epsilon-connected ordinal set

rng C is set

C is Element of the carrier of A

O is set

C . O is set

p9 is epsilon-transitive epsilon-connected ordinal set

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

(A,f,gf,p9) is Element of the carrier of A

f . (A,f,gf,g) is Element of the carrier of A

f . (A,f,gf,p9) is Element of the carrier of A

(A,f,gf,(succ p9)) is Element of the carrier of A

"/\" ((rng C),A) is Element of the carrier of A

{ b

"\/" ( { b

C is epsilon-transitive epsilon-connected ordinal set

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

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty trivial 1 -element set

C \/ {C} is non empty set

(A,f,gf,C) is Element of the carrier of A

f . (A,f,gf,g) is Element of the carrier of A

f . (A,f,gf,C) is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is Element of the carrier of A

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is Element of the carrier of A

c

C is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,C) is Element of the carrier of A

(A,f,gf,c

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

f . gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is Element of the carrier of A

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is Element of the carrier of A

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

{g} is non empty trivial 1 -element set

g \/ {g} is non empty set

(A,f,gf,(succ g)) is Element of the carrier of A

f . (A,f,gf,g) is Element of the carrier of A

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

f . gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,g) is Element of the carrier of A

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is Element of the carrier of A

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

{g} is non empty trivial 1 -element set

g \/ {g} is non empty set

(A,f,gf,(succ g)) is Element of the carrier of A

f . (A,f,gf,g) is Element of the carrier of A

A is epsilon-transitive epsilon-connected ordinal set

f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of f is non empty set

[: the carrier of f, the carrier of f:] is non empty set

bool [: the carrier of f, the carrier of f:] is non empty set

gf is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone Element of bool [: the carrier of f, the carrier of f:]

g is Element of the carrier of f

gf . g is Element of the carrier of f

(f,gf,g,A) is Element of the carrier of f

c

(f,gf,g,c

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

dom C is epsilon-transitive epsilon-connected ordinal set

rng C is set

C is Element of the carrier of f

O is set

C . O is set

p9 is epsilon-transitive epsilon-connected ordinal set

(f,gf,g,p9) is Element of the carrier of f

p9 is epsilon-transitive epsilon-connected ordinal set

(f,gf,g,p9) is Element of the carrier of f

p9 is epsilon-transitive epsilon-connected ordinal set

"\/" ((rng C),f) is Element of the carrier of f

c

(f,gf,g,c

succ c

(f,gf,g,(succ c

gf . (f,gf,g,c

(f,gf,g,{}) is Element of the carrier of f

A is epsilon-transitive epsilon-connected ordinal set

f is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of f is non empty set

[: the carrier of f, the carrier of f:] is non empty set

bool [: the carrier of f, the carrier of f:] is non empty set

gf is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone Element of bool [: the carrier of f, the carrier of f:]

g is Element of the carrier of f

gf . g is Element of the carrier of f

(f,gf,g,A) is Element of the carrier of f

c

(f,gf,g,c

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

dom C is epsilon-transitive epsilon-connected ordinal set

rng C is set

C is Element of the carrier of f

O is set

C . O is set

p9 is epsilon-transitive epsilon-connected ordinal set

(f,gf,g,p9) is Element of the carrier of f

p9 is epsilon-transitive epsilon-connected ordinal set

(f,gf,g,p9) is Element of the carrier of f

p9 is epsilon-transitive epsilon-connected ordinal set

"/\" ((rng C),f) is Element of the carrier of f

{ b

"\/" ( { b

c

(f,gf,g,c

succ c

(f,gf,g,(succ c

gf . (f,gf,g,c

(f,gf,g,{}) is Element of the carrier of f

A is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

card the carrier of A is epsilon-transitive epsilon-connected ordinal non empty cardinal set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

f . gf is Element of the carrier of A

nextcard (card the carrier of A) is epsilon-transitive epsilon-connected ordinal cardinal set

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

dom C is epsilon-transitive epsilon-connected ordinal set

C is set

O is set

C . C is set

C . O is set

p9 is epsilon-transitive epsilon-connected ordinal set

C . p9 is set

(A,f,gf,p9) is Element of the carrier of A

p is epsilon-transitive epsilon-connected ordinal set

C . p is set

(A,f,gf,p) is Element of the carrier of A

rng C is set

C is set

O is set

C . O is set

p9 is epsilon-transitive epsilon-connected ordinal set

C . p9 is set

(A,f,gf,p9) is Element of the carrier of A

card (nextcard (card the carrier of A)) is epsilon-transitive epsilon-connected ordinal cardinal set

C is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,C) is Element of the carrier of A

C is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,C) is Element of the carrier of A

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

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

card the carrier of A is epsilon-transitive epsilon-connected ordinal non empty cardinal set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

f . gf is Element of the carrier of A

nextcard (card the carrier of A) is epsilon-transitive epsilon-connected ordinal cardinal set

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

dom C is epsilon-transitive epsilon-connected ordinal set

C is set

O is set

C . C is set

C . O is set

p9 is epsilon-transitive epsilon-connected ordinal set

C . p9 is set

(A,f,gf,p9) is Element of the carrier of A

p is epsilon-transitive epsilon-connected ordinal set

C . p is set

(A,f,gf,p) is Element of the carrier of A

rng C is set

C is set

O is set

C . O is set

p9 is epsilon-transitive epsilon-connected ordinal set

C . p9 is set

(A,f,gf,p9) is Element of the carrier of A

card (nextcard (card the carrier of A)) is epsilon-transitive epsilon-connected ordinal cardinal set

C is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,C) is Element of the carrier of A

C is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,C) is Element of the carrier of A

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

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

card the carrier of A is epsilon-transitive epsilon-connected ordinal non empty cardinal set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

g is Element of the carrier of A

gf "\/" g is Element of the carrier of A

gg is Element of the carrier of A

f . gf is Element of the carrier of A

f . gg is Element of the carrier of A

f . g is Element of the carrier of A

c

card c

(A,f,gg,c

(A,f,(gf "\/" g),c

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

card the carrier of A is epsilon-transitive epsilon-connected ordinal non empty cardinal set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

g is Element of the carrier of A

gf "/\" g is Element of the carrier of A

gg is Element of the carrier of A

f . gg is Element of the carrier of A

f . gf is Element of the carrier of A

f . g is Element of the carrier of A

c

card c

(A,f,gg,c

(A,f,(gf "/\" g),c

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

g is Element of the carrier of A

f . g is Element of the carrier of A

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,gg) is Element of the carrier of A

f . (A,f,gf,gg) is Element of the carrier of A

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

(A,f,gf,(succ gg)) is Element of the carrier of A

gg is epsilon-transitive epsilon-connected ordinal set

c

dom c

rng c

C is Element of the carrier of A

C is set

c

O is epsilon-transitive epsilon-connected ordinal set

(A,f,gf,O) is Element of the carrier of A

(A,f,gf,gg) is Element of the carrier of A

"\/" ((rng c

(A,f,gf,{}) is Element of the carrier of A

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

gf is Element of the carrier of A

g is Element of the carrier of A

f . gf is Element of the carrier of A

gg is epsilon-transitive epsilon-connected ordinal set

(A,f,g,gg) is Element of the carrier of A

f . (A,f,g,gg) is Element of the carrier of A

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

(A,f,g,(succ gg)) is Element of the carrier of A

gg is epsilon-transitive epsilon-connected ordinal set

c

dom c

rng c

C is Element of the carrier of A

C is set

c

O is epsilon-transitive epsilon-connected ordinal set

(A,f,g,O) is Element of the carrier of A

(A,f,g,gg) is Element of the carrier of A

"/\" ((rng c

{ b

"\/" ( { b

(A,f,g,{}) is Element of the carrier of A

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of A:]

bool the carrier of A is non empty set

{ b

{ b

g is Element of the carrier of A

gg is Element of bool the carrier of A

c

C is Element of the carrier of A

C is Element of the carrier of A

O is Element of the carrier of A

p9 is Element of the carrier of A

p is Element of the carrier of A

p9 "\/" p is Element of the carrier of A

card the carrier of A is epsilon-transitive epsilon-connected ordinal non empty cardinal set

r is Element of the carrier of A

r99 is epsilon-transitive epsilon-connected ordinal set

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

(A,f,r,r99) is Element of the carrier of A

q is Element of the carrier of A

q99 is Element of the carrier of A

c

C is Element of the carrier of A

C is Element of the carrier of A

O is Element of the carrier of A

p9 is Element of the carrier of A

p is Element of the carrier of A

p9 "/\" p is Element of the carrier of A

card the carrier of A is epsilon-transitive epsilon-connected ordinal non empty cardinal set

r is Element of the carrier of A

r99 is epsilon-transitive epsilon-connected ordinal set

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

(A,f,r,r99) is Element of the carrier of A

q is Element of the carrier of A

q99 is Element of the carrier of A

c

(A,c

gg is non empty (A) (A) Element of bool the carrier of A

gf is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

(A,gg) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

c

g is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

(A,c

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

(A,f) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of (A,f) is non empty set

{ b

bool the carrier of A is non empty set

gf is non empty (A) (A) Element of bool the carrier of A

(A,gf) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

(A,f) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of (A,f) is non empty set

{ b

gf is set

g is Element of the carrier of A

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

(A,f) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of (A,f) is non empty set

gf is Element of the carrier of A

{ b

g is Element of the carrier of A

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

(A,f) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of (A,f) is non empty set

bool the carrier of A is non empty set

{ b

gf is Element of the carrier of (A,f)

g is Element of the carrier of (A,f)

gg is Element of the carrier of A

c

C is non empty (A) (A) Element of bool the carrier of A

(A,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

C is Element of the carrier of A

C is Element of the carrier of A

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

(A,f) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of (A,f) is non empty set

c

c

"\/" ((c

f . ("\/" ((c

O is Element of the carrier of A

f . O is Element of the carrier of A

p9 is Element of the carrier of A

card the carrier of A is epsilon-transitive epsilon-connected ordinal non empty cardinal set

O is epsilon-transitive epsilon-connected ordinal set

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

(A,f,("\/" ((c

p9 is Element of the carrier of A

p is Element of the carrier of (A,f)

r is Element of the carrier of (A,f)

r99 is Element of the carrier of A

r is Element of the carrier of (A,f)

{ b

r9 is Element of the carrier of A

q is Element of the carrier of A

q99 is Element of the carrier of (A,f)

r99 is Element of the carrier of (A,f)

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

Bottom A is Element of the carrier of A

nextcard the carrier of A is epsilon-transitive epsilon-connected ordinal cardinal set

(A,f,(Bottom A),(nextcard the carrier of A)) is Element of the carrier of A

Top A is Element of the carrier of A

(A,f,(Top A),(nextcard the carrier of A)) is Element of the carrier of A

A is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr

the carrier of A is non empty set

[: the carrier of A, the carrier of A:] is non empty set

bool [: the carrier of A, the carrier of A:] is non empty set

card the carrier of A is epsilon-transitive epsilon-connected ordinal non empty cardinal set

Bottom A is Element of the carrier of A

f is Relation-like the carrier of A -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of A, the carrier of A:]

(A,f) is Element of the carrier of A

nextcard the carrier of A is epsilon-transitive epsilon-connected ordinal cardinal set

(A,f,(Bottom A),(nextcard the carrier of A)) is Element of the carrier of A

gf is Element of the carrier of A

f . gf is Element of the carrier of A

g is epsilon-transitive epsilon-connected ordinal set

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

(A,f,(Bottom A),g) is Element of the carrier of A

A is non empty join-commutative