:: 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₆ is set
gf . c₆ is set
[c₆,g] is set
{c₆,g} is non empty set
{c₆} is non empty trivial 1 -element set
{{c₆,g},{c₆}} is non empty set
A . c₆ is set
[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₆ is set
g . gg is set
g . c₆ is set
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₁ where b₁ is Element of bool A : f . b₁ c= b₁ } is set
meet { b₁ where b₁ is Element of bool A : f . b₁ c= b₁ } is set
{ b₁ where b₁ is Element of bool A : S₁[b₁] } is set
gf is Element of bool (bool A)
g is Element of bool (bool A)
meet g is Element of bool A
{ b₁ where b₁ is Element of bool A : b₁ c= f . b₁ } is set
union { b₁ where b₁ is Element of bool A : b₁ c= f . b₁ } is set
{ b₁ where b₁ is Element of bool A : S₁[b₁] } is set
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₁ where b₁ is Element of bool A : f . b₁ c= b₁ } is set
meet { b₁ where b₁ is Element of bool A : f . b₁ c= b₁ } is set
{ b₁ where b₁ is Element of bool A : S₁[b₁] } is set
gf is Element of bool (bool A)
g is Element of bool (bool A)
meet g is Element of bool A
c₆ is Element of bool A
f . c₆ is Element of bool A
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₁ where b₁ is Element of bool A : b₁ c= f . b₁ } is set
union { b₁ where b₁ is Element of bool A : b₁ c= f . b₁ } is set
{ b₁ where b₁ is Element of bool A : S₁[b₁] } is set
gf is Element of bool (bool A)
union gf is Element of bool A
gg is set
c₆ is Element of bool A
f . c₆ is Element of bool A
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₁ where b₁ is Element of bool A : f . b₁ c= b₁ } is set
meet { b₁ where b₁ is Element of bool A : f . b₁ c= b₁ } is set
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₁ where b₁ is Element of bool A : b₁ c= f . b₁ } is set
union { b₁ where b₁ is Element of bool A : b₁ c= f . b₁ } is set
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₁ where b₁ is Element of bool A : f . b₁ c= b₁ } is set
meet { b₁ where b₁ is Element of bool A : f . b₁ c= b₁ } is set
(A,f) is Element of bool A
{ b₁ where b₁ is Element of bool A : b₁ c= f . b₁ } is set
union { b₁ where b₁ is Element of bool A : b₁ c= f . b₁ } is set
gf is Element of bool A
f . gf is Element of bool A
F₁() is set
F₂(F₁()) is set
bool F₁() is non empty Element of bool (bool F₁())
bool F₁() is non empty set
bool (bool F₁()) is non empty set
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₂(gf) is set
[:(bool F₁()),(bool F₁()):] is non empty set
bool [:(bool F₁()),(bool F₁()):] is non empty set
gf is set
f is Relation-like bool F₁() -defined bool F₁() -valued Function-like quasi_total Element of bool [:(bool F₁()),(bool F₁()):]
dom f is Element of bool (bool F₁())
bool (bool F₁()) is non empty set
g is set
f . gf is set
F₂(gf) is set
f . g is set
F₂(g) is set
gf is Relation-like bool F₁() -defined bool F₁() -valued Function-like quasi_total c=-monotone Element of bool [:(bool F₁()),(bool F₁()):]
(F₁(),gf) is Element of bool F₁()
{ b₁ where b₁ is Element of bool F₁() : gf . b₁ c= b₁ } is set
meet { b₁ where b₁ is Element of bool F₁() : gf . b₁ c= b₁ } is set
g is Element of bool F₁()
F₂(g) is set
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₆ is set
dom gg is Element of bool (bool A)
bool (bool A) is non empty set
C is set
gf .: c₆ is Element of bool f
bool f is non empty set
gf .: C is Element of bool f
f \ (gf .: C) is Element of bool f
f \ (gf .: c₆) is Element of bool f
g .: (f \ (gf .: C)) is Element of bool A
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
gg . c₆ is set
gg . C is set
c₆ is Relation-like bool A -defined bool A -valued Function-like quasi_total c=-monotone Element of bool [:(bool A),(bool A):]
(A,c₆) is Element of bool A
{ b₁ where b₁ is Element of bool A : c₆ . b₁ c= b₁ } is set
meet { b₁ where b₁ is Element of bool A : c₆ . b₁ c= b₁ } is set
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₆ . C is Element of bool A
A \ (c₆ . C) is Element of bool A
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₆ is set
C is set
C is set
gg \/ c₆ is set
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₆ is set
dom g is Element of bool A
bool A is non empty set
[gg,c₆] is set
{gg,c₆} is non empty set
{gg} is non empty trivial 1 -element set
{{gg,c₆},{gg}} is non empty set
gg is set
c₆ is set
g . c₆ is set
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₆ is set
[gg,c₆] is set
{gg,c₆} is non empty set
{gg} is non empty trivial 1 -element set
{{gg,c₆},{gg}} is non empty set
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₆ 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
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₆ 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
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₆ is epsilon-transitive epsilon-connected ordinal set
succ c₆ is epsilon-transitive epsilon-connected ordinal non empty set
C . {} 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
(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₆ is epsilon-transitive epsilon-connected ordinal set
succ c₆ is epsilon-transitive epsilon-connected ordinal non empty set
C . {} 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₆ is set
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₆ is set
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₆ is epsilon-transitive epsilon-connected ordinal set
(A,f,gf,c₆) is set
succ c₆ is epsilon-transitive epsilon-connected ordinal non empty 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
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₁ where b₁ is Element of the carrier of A : b₁ is_less_than rng gg } is set
"\/" ( { b₁ where b₁ is Element of the carrier of A : b₁ is_less_than rng gg } ,A) is Element of the carrier of A
C is set
c₆ is epsilon-transitive epsilon-connected ordinal set
(A,f,gf,c₆) is set
succ c₆ is epsilon-transitive epsilon-connected ordinal non empty 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
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₆ is Element of the carrier of A
f . c₆ is Element of the carrier of A
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₆ is Relation-like Function-like T-Sequence-like set
dom c₆ is epsilon-transitive epsilon-connected ordinal set
(A,f,gf,gg) is set
rng c₆ is set
"\/" ((rng c₆),A) is Element of the carrier of A
(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₆ is Element of the carrier of A
f . c₆ is Element of the carrier of A
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₆ is Relation-like Function-like T-Sequence-like set
dom c₆ is epsilon-transitive epsilon-connected ordinal set
(A,f,gf,gg) is set
rng c₆ is set
"/\" ((rng c₆),A) is Element of the carrier of A
{ b₁ where b₁ is Element of the carrier of A : b₁ is_less_than rng c₆ } is set
"\/" ( { b₁ where b₁ is Element of the carrier of A : b₁ is_less_than rng c₆ } ,A) is Element of the carrier of A
(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₆ is Element of 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₆ 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 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₆ is Relation-like f -defined f -valued Element of bool [:f,f:]
field c₆ is set
dom c₆ is set
rng c₆ is set
(dom c₆) \/ (rng 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
dom c₆ is Element of bool f
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₁,b₂] where b₁, b₂ is Element of the carrier of g : b₁ [= b₂ } is set
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₁,b₂] where b₁, b₂ is Element of the carrier of gf : b₁ [= b₂ } is set
gg is set
c₆ is Element of the carrier of gf
C is Element of the carrier of gf
[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
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₆ is Element of the carrier of g
C is Element of the carrier of g
[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
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₁ where b₁ is Element of the carrier of A : b₁ [= f . b₁ } is set
{ (f . b₁) where b₁ is Element of the carrier of A : b₁ [= f . b₁ } is set
"\/" ( { b₁ where b₁ is Element of the carrier of A : b₁ [= f . b₁ } ,A) is Element of the carrier of A
"\/" ( { (f . b₁) where b₁ is Element of the carrier of A : b₁ [= f . b₁ } ,A) is Element of the carrier of A
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₁ where b₁ is Element of the carrier of A : b₁ [= f . b₁ } ,A)) is Element of the carrier of A
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₁ where b₁ is Element of the carrier of A : b₁ [= f . b₁ } ,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
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₆ is epsilon-transitive epsilon-connected ordinal set
(A,f,gf,c₆) 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
C . c₆ is set
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₆ is epsilon-transitive epsilon-connected ordinal set
(A,f,gf,c₆) 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
C . c₆ is set
rng C is set
"/\" ((rng C),A) is Element of the carrier of A
{ b₁ where b₁ is Element of the carrier of A : b₁ is_less_than rng C } is set
"\/" ( { b₁ where b₁ is Element of the carrier of A : b₁ is_less_than 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 epsilon-transitive epsilon-connected ordinal set
(A,f,gf,gg) 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
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₆ is epsilon-transitive epsilon-connected ordinal set
(A,f,gf,c₆) is Element of the carrier of A
(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₆ is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
(A,f,gf,c₆) is Element of the carrier of A
(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₆ is epsilon-transitive epsilon-connected ordinal set
(A,f,gf,c₆) 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
C . gg is set
rng C is set
"/\" ((rng C),A) is Element of the carrier of A
{ b₁ where b₁ is Element of the carrier of A : b₁ is_less_than rng C } is set
"\/" ( { b₁ where b₁ is Element of the carrier of A : b₁ is_less_than 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₆ is epsilon-transitive epsilon-connected ordinal set
(A,f,gf,c₆) is Element of the carrier of A
(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₁ where b₁ is Element of the carrier of A : b₁ is_less_than rng C } is set
"\/" ( { b₁ where b₁ is Element of the carrier of A : b₁ is_less_than 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,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₆ is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
(A,f,gf,C) is Element of the carrier of A
(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
(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₆ is epsilon-transitive epsilon-connected ordinal set
(f,gf,g,c₆) is Element of the carrier of f
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₆ is epsilon-transitive epsilon-connected ordinal set
(f,gf,g,c₆) is Element of the carrier of f
succ c₆ is epsilon-transitive epsilon-connected ordinal non empty set
(f,gf,g,(succ c₆)) is Element of the carrier of f
gf . (f,gf,g,c₆) is Element of the carrier of f
(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₆ is epsilon-transitive epsilon-connected ordinal set
(f,gf,g,c₆) is Element of the carrier of f
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₁ where b₁ is Element of the carrier of f : b₁ is_less_than rng C } is set
"\/" ( { b₁ where b₁ is Element of the carrier of f : b₁ is_less_than rng C } ,f) is Element of the carrier of f
c₆ is epsilon-transitive epsilon-connected ordinal set
(f,gf,g,c₆) is Element of the carrier of f
succ c₆ is epsilon-transitive epsilon-connected ordinal non empty set
(f,gf,g,(succ c₆)) is Element of the carrier of f
gf . (f,gf,g,c₆) is Element of the carrier of f
(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₆ is epsilon-transitive epsilon-connected ordinal set
card c₆ is epsilon-transitive epsilon-connected ordinal cardinal set
(A,f,gg,c₆) is Element of the carrier of A
(A,f,(gf "\/" g),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
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₆ is epsilon-transitive epsilon-connected ordinal set
card c₆ is epsilon-transitive epsilon-connected ordinal cardinal set
(A,f,gg,c₆) is Element of the carrier of A
(A,f,(gf "/\" g),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
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₆ 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
C is set
c₆ . C is set
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) 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
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₆ 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
C is set
c₆ . C is set
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₆),A) is Element of the carrier of A
{ b₁ where b₁ is Element of the carrier of A : b₁ is_less_than rng c₆ } is set
"\/" ( { b₁ where b₁ is Element of the carrier of A : b₁ is_less_than rng c₆ } ,A) is Element of the carrier of A
(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₁ where b₁ is Element of the carrier of A : b₁ is_a_fixpoint_of f } is set
{ b₁ where b₁ is Element of the carrier of A : S₁[b₁] } is set
g is Element of the carrier of A
gg is Element of bool the carrier of A
c₆ is Element of the carrier of A
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₆ is Element of the carrier of A
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₆ 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
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₆ is non empty (A) (A) Element of bool the carrier of A
g is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(A,c₆) 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₁ where b₁ is Element of the carrier of A : b₁ is_a_fixpoint_of f } is set
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₁ where b₁ is Element of the carrier of A : b₁ is_a_fixpoint_of f } is set
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₁ where b₁ is Element of the carrier of A : b₁ is_a_fixpoint_of f } 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
bool the carrier of A is non empty set
{ b₁ where b₁ is Element of the carrier of A : b₁ is_a_fixpoint_of f } is set
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₆ is Element of the carrier of A
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₆ is set
c₆ /\ the carrier of (A,f) is set
"\/" ((c₆ /\ the carrier of (A,f)),A) is Element of the carrier of A
f . ("\/" ((c₆ /\ the carrier of (A,f)),A)) is Element of the carrier of A
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₆ /\ the carrier of (A,f)),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,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₁ where b₁ is Element of the carrier of A : b₁ is_a_fixpoint_of f } is set
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 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
Top 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,(Top 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,(Top A),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 Element of 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
(A,f) 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
gf is Element of the carrier of A
g is epsilon-transitive epsilon-connected ordinal set
gg is Relation-like Function-like T-Sequence-like set
dom gg is epsilon-transitive epsilon-connected ordinal set
rng gg is set
c₆ is Element of the carrier of A
C is set
gg . C is set
C is epsilon-transitive epsilon-connected ordinal set
(A,f,(Bottom A),C) is Element of the carrier of A
(A,f,(Bottom A),g) is Element of the carrier of A
"\/" ((rng gg),A) 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,(Bottom A),g) is Element of the carrier of A
f . (A,f,(Bottom A),g) is Element of the carrier of A
succ g is epsilon-transitive epsilon-connected ordinal non empty set
(A,f,(Bottom A),(succ g)) is Element of the carrier of A
(A,f,(Bottom A),{}) is Element of the carrier of A
g is epsilon-transitive epsilon-connected ordinal set
(A,f,(Top A),g) is Element of the carrier of A
f . (A,f,(Top A),g) is Element of the carrier of A
succ g is epsilon-transitive epsilon-connected ordinal non empty set
(A,f,(Top A),(succ g)) is Element of the carrier of A
g is epsilon-transitive epsilon-connected ordinal set
gg is Relation-like Function-like T-Sequence-like set
dom gg is epsilon-transitive epsilon-connected ordinal set
rng gg is set
c₆ is Element of the carrier of A
C is set
gg . C is set
C is epsilon-transitive epsilon-connected ordinal set
(A,f,(Top A),C) is Element of the carrier of A
(A,f,(Top A),g) is Element of the carrier of A
"/\" ((rng gg),A) is Element of the carrier of A
{ b₁ where b₁ is Element of the carrier of A : b₁ is_less_than rng gg } is set
"\/" ( { b₁ where b₁ is Element of the carrier of A : b₁ is_less_than rng gg } ,A) is Element of the carrier of A
(A,f,(Top 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
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
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
gf is Element of the carrier of A
f . gf is Element of the carrier of A
card the carrier of A is epsilon-transitive epsilon-connected ordinal non empty cardinal set
g is epsilon-transitive epsilon-connected ordinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
(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:]
(A,f) is Element of the carrier of A
Top A is Element of the carrier of A
nextcard the carrier of A is epsilon-transitive epsilon-connected ordinal cardinal set
(A,f,(Top 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
card the carrier of A is epsilon-transitive epsilon-connected ordinal non empty cardinal set
g is epsilon-transitive epsilon-connected ordinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
(A,f,gf,g) is Element of the carrier of A
A is non empty set
BooleLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean complete LattStr
the carrier of (BooleLatt A) is non empty set
[: the carrier of (BooleLatt A), the carrier of (BooleLatt A):] is non empty set
bool [: the carrier of (BooleLatt A), the carrier of (BooleLatt A):] is non empty set
f is Relation-like the carrier of (BooleLatt A) -defined the carrier of (BooleLatt A) -valued Function-like quasi_total Element of bool [: the carrier of (BooleLatt A), the carrier of (BooleLatt A):]
gf is Element of the carrier of (BooleLatt A)
g is Element of the carrier of (BooleLatt A)
f . gf is Element of the carrier of (BooleLatt A)
f . g is Element of the carrier of (BooleLatt A)
gf is Element of the carrier of (BooleLatt A)
g is Element of the carrier of (BooleLatt A)
f . gf is Element of the carrier of (BooleLatt A)
f . g is Element of the carrier of (BooleLatt A)
A is non empty set
BooleLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean complete LattStr
the carrier of (BooleLatt A) is non empty set
[: the carrier of (BooleLatt A), the carrier of (BooleLatt A):] is non empty set
bool [: the carrier of (BooleLatt A), the carrier of (BooleLatt A):] is non empty 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 the carrier of (BooleLatt A) -defined the carrier of (BooleLatt A) -valued Function-like quasi_total monotone Element of bool [: the carrier of (BooleLatt A), the carrier of (BooleLatt A):]
((BooleLatt A),f) is Element of the carrier of (BooleLatt A)
Bottom (BooleLatt A) is Element of the carrier of (BooleLatt A)
nextcard the carrier of (BooleLatt A) is epsilon-transitive epsilon-connected ordinal cardinal set
((BooleLatt A),f,(Bottom (BooleLatt A)),(nextcard the carrier of (BooleLatt A))) is Element of the carrier of (BooleLatt A)
g is Relation-like bool A -defined bool A -valued Function-like quasi_total c=-monotone Element of bool [:(bool A),(bool A):]
(A,g) is Element of bool A
{ b₁ where b₁ is Element of bool A : g . b₁ c= b₁ } is set
meet { b₁ where b₁ is Element of bool A : g . b₁ c= b₁ } is set
gg is Element of the carrier of (BooleLatt A)
gf is Element of bool A
A is non empty set
BooleLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean complete LattStr
the carrier of (BooleLatt A) is non empty set
[: the carrier of (BooleLatt A), the carrier of (BooleLatt A):] is non empty set
bool [: the carrier of (BooleLatt A), the carrier of (BooleLatt A):] is non empty 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 the carrier of (BooleLatt A) -defined the carrier of (BooleLatt A) -valued Function-like quasi_total monotone Element of bool [: the carrier of (BooleLatt A), the carrier of (BooleLatt A):]
((BooleLatt A),f) is Element of the carrier of (BooleLatt A)
Top (BooleLatt A) is Element of the carrier of (BooleLatt A)
nextcard the carrier of (BooleLatt A) is epsilon-transitive epsilon-connected ordinal cardinal set
((BooleLatt A),f,(Top (BooleLatt A)),(nextcard the carrier of (BooleLatt A))) is Element of the carrier of (BooleLatt A)
g is Relation-like bool A -defined bool A -valued Function-like quasi_total c=-monotone Element of bool [:(bool A),(bool A):]
(A,g) is Element of bool A
{ b₁ where b₁ is Element of bool A : b₁ c= g . b₁ } is set
union { b₁ where b₁ is Element of bool A : b₁ c= g . b₁ } is set
gg is Element of the carrier of (BooleLatt A)
gf is Element of bool A