:: KNASTER semantic presentation

REAL is set

bool REAL is non empty set

bool NAT is non empty V50() set
bool NAT is non empty V50() set

dom f is set
rng f is 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
c6 is set
gf . c6 is set
[c6,g] is set
{c6,g} is non empty set
{c6} is non empty trivial 1 -element set
{{c6,g},{c6}} is non empty set
A . c6 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

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

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

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

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

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

gg is set
dom g is set
c6 is set
g . gg is set
g . c6 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

{ b1 where b1 is Element of bool A : f . b1 c= b1 } is set
meet { b1 where b1 is Element of bool A : f . b1 c= b1 } is set
{ b1 where b1 is Element of bool A : S1[b1] } is set
gf is Element of bool (bool A)
g is Element of bool (bool A)
meet g is Element of bool A
{ b1 where b1 is Element of bool A : b1 c= f . b1 } is set
union { b1 where b1 is Element of bool A : b1 c= f . b1 } is set
{ b1 where b1 is Element of bool A : S1[b1] } 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

(A,f) is Element of bool A
{ b1 where b1 is Element of bool A : f . b1 c= b1 } is set
meet { b1 where b1 is Element of bool A : f . b1 c= b1 } is set
{ b1 where b1 is Element of bool A : S1[b1] } is set
gf is Element of bool (bool A)
g is Element of bool (bool A)
meet g is Element of bool A
c6 is Element of bool A
f . c6 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

(A,f) is Element of bool A
{ b1 where b1 is Element of bool A : b1 c= f . b1 } is set
union { b1 where b1 is Element of bool A : b1 c= f . b1 } is set
{ b1 where b1 is Element of bool A : S1[b1] } is set
gf is Element of bool (bool A)
union gf is Element of bool A
gg is set
c6 is Element of bool A
f . c6 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

(A,f) is Element of bool A
{ b1 where b1 is Element of bool A : f . b1 c= b1 } is set
meet { b1 where b1 is Element of bool A : f . b1 c= b1 } 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

(A,f) is Element of bool A
{ b1 where b1 is Element of bool A : b1 c= f . b1 } is set
union { b1 where b1 is Element of bool A : b1 c= f . b1 } 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

(A,f) is Element of bool A
{ b1 where b1 is Element of bool A : f . b1 c= b1 } is set
meet { b1 where b1 is Element of bool A : f . b1 c= b1 } is set
(A,f) is Element of bool A
{ b1 where b1 is Element of bool A : b1 c= f . b1 } is set
union { b1 where b1 is Element of bool A : b1 c= f . b1 } is set
gf is Element of bool A
f . gf is Element of bool A
F1() is set
F2(F1()) is set
bool F1() is non empty Element of bool (bool F1())
bool F1() is non empty set
bool (bool F1()) is non empty set

dom A is set
rng A is set
f is set
gf is set
A . gf is set
F2(gf) is set
[:(bool F1()),(bool F1()):] is non empty set
bool [:(bool F1()),(bool F1()):] is non empty set
gf is set
f is Relation-like bool F1() -defined bool F1() -valued Function-like quasi_total Element of bool [:(bool F1()),(bool F1()):]
dom f is Element of bool (bool F1())
bool (bool F1()) is non empty set
g is set
f . gf is set
F2(gf) is set
f . g is set
F2(g) is set
gf is Relation-like bool F1() -defined bool F1() -valued Function-like quasi_total c=-monotone Element of bool [:(bool F1()),(bool F1()):]
(F1(),gf) is Element of bool F1()
{ b1 where b1 is Element of bool F1() : gf . b1 c= b1 } is set
meet { b1 where b1 is Element of bool F1() : gf . b1 c= b1 } is set
g is Element of bool F1()
F2(g) is set
gf . g is Element of bool F1()
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

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

c6 is set
dom gg is Element of bool (bool A)
bool (bool A) is non empty set
C is set
gf .: c6 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 .: c6) is Element of bool f
g .: (f \ (gf .: C)) is Element of bool A
g .: (f \ (gf .: c6)) is Element of bool A
A \ (g .: (f \ (gf .: c6))) is Element of bool A
A \ (g .: (f \ (gf .: C))) is Element of bool A
gg . c6 is set
gg . C is set

(A,c6) is Element of bool A
{ b1 where b1 is Element of bool A : c6 . b1 c= b1 } is set
meet { b1 where b1 is Element of bool A : c6 . b1 c= b1 } 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
c6 . C is Element of bool A
A \ (c6 . 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

gg is set
c6 is set
C is set
C is set
gg \/ c6 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

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

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

rng g is Element of bool f
bool f is non empty set
gg is set
g . gg is set
c6 is set
dom g is Element of bool A
bool A is non empty set
[gg,c6] is set
{gg,c6} is non empty set
{gg} is non empty trivial 1 -element set
{{gg,c6},{gg}} is non empty set
gg is set
c6 is set
g . c6 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
c6 is set
[gg,c6] is set
{gg,c6} is non empty set
{gg} is non empty trivial 1 -element set
{{gg,c6},{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

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

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

last C is set

C . {} is set
rng C is set
c6 is set

last C is set

C . {} is set
rng C is set
O is set

last p9 is set

p9 . {} is set
gg is set

last C is set

C . {} is set
rng C is set
c6 is set

last C is set

C . {} is set
rng C is set
O is set

last p9 is set

p9 . {} is set

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

(A,f,gf,g) is set

C is set

last C is set

C . {} is set
(A,f,gf,c6) is set

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

(A,f,gf,g) is set

C is set

last C is set

C . {} is set
(A,f,gf,c6) is set

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,(succ g)) is set
(A,f,gf,g) is set
f . (A,f,gf,g) is set
c6 is set

(A,f,gf,gg) is set

C is set

last O is set

O . {} is set
(A,f,gf,C) is set

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,(succ g)) is set
(A,f,gf,g) is set
f . (A,f,gf,g) is set
c6 is set

(A,f,gf,gg) is set

C is set

last O is set

O . {} is set
(A,f,gf,C) is set

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,g) is set

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

(A,f,gf,c6) is set

O is set

last p9 is set

p9 . {} is set
(A,f,gf,C) is set

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,g) is set

rng gg is set
"/\" ((rng gg),A) is Element of the carrier of A
{ b1 where b1 is Element of the carrier of A : b1 is_less_than rng gg } is set
"\/" ( { b1 where b1 is Element of the carrier of A : b1 is_less_than rng gg } ,A) is Element of the carrier of A
C is set

(A,f,gf,c6) is set

O is set

last p9 is set

p9 . {} is set
(A,f,gf,C) is set

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

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

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

(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

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

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

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

(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

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,g) is set

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

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

(A,f,gf,gg) is set
rng c6 is set
"\/" ((rng c6),A) is Element of the carrier of A
(A,f,gf,{}) is set

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,g) is set

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

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

(A,f,gf,gg) is set
rng c6 is set
"/\" ((rng c6),A) is Element of the carrier of A
{ b1 where b1 is Element of the carrier of A : b1 is_less_than rng c6 } is set
"\/" ( { b1 where b1 is Element of the carrier of A : b1 is_less_than rng c6 } ,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

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
c6 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
c6 is Element of the carrier of A

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
() |_2 f is Relation-like set
[:f,f:] is non empty set
() /\ [:f,f:] is set
bool [:f,f:] is non empty set
field () is set
dom () is set
rng () is set
(dom ()) \/ (rng ()) is set
c6 is Relation-like f -defined f -valued Element of bool [:f,f:]
field c6 is set
dom c6 is set
rng c6 is set
(dom c6) \/ (rng c6) 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 c6 is Element of bool f
bool f is non empty set

RelStr(# f,C #) is strict RelStr

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

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,() #) 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

the carrier of gf is non empty set

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
{ [b1,b2] where b1, b2 is Element of the carrier of g : b1 [= b2 } 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
{ [b1,b2] where b1, b2 is Element of the carrier of gf : b1 [= b2 } is set
gg is set
c6 is Element of the carrier of gf
C is Element of the carrier of gf
[c6,C] is set
{c6,C} is non empty set
{c6} is non empty trivial 1 -element set
{{c6,C},{c6}} 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
c6 is Element of the carrier of g
C is Element of the carrier of g
[c6,C] is set
{c6,C} is non empty set
{c6} is non empty trivial 1 -element set
{{c6,C},{c6}} 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

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

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

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:]
{ b1 where b1 is Element of the carrier of A : b1 [= f . b1 } is set
{ (f . b1) where b1 is Element of the carrier of A : b1 [= f . b1 } is set
"\/" ( { b1 where b1 is Element of the carrier of A : b1 [= f . b1 } ,A) is Element of the carrier of A
"\/" ( { (f . b1) where b1 is Element of the carrier of A : b1 [= f . b1 } ,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 . ("\/" ( { b1 where b1 is Element of the carrier of A : b1 [= f . b1 } ,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 . ("\/" ( { b1 where b1 is Element of the carrier of A : b1 [= f . b1 } ,A))) is Element of the carrier of A

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

gg is set

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

C . c6 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

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

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

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

gg is set

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

C . c6 is set
rng C is set
"/\" ((rng C),A) is Element of the carrier of A
{ b1 where b1 is Element of the carrier of A : b1 is_less_than rng C } is set
"\/" ( { b1 where b1 is Element of the carrier of A : b1 is_less_than rng C } ,A) is Element of the carrier of A
(A,f,gf,g) is Element of the carrier of A

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

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

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

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

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

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

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

(A,f,gf,c6) 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

rng C is set
C is Element of the carrier of A
O is set
C . O is 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 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

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

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

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

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

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

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

C . gg is set
rng C is set
"/\" ((rng C),A) is Element of the carrier of A
{ b1 where b1 is Element of the carrier of A : b1 is_less_than rng C } is set
"\/" ( { b1 where b1 is Element of the carrier of A : b1 is_less_than rng C } ,A) is Element of the carrier of A

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

(A,f,gf,c6) 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

rng C is set
C is Element of the carrier of A
O is set
C . O is 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
{ b1 where b1 is Element of the carrier of A : b1 is_less_than rng C } is set
"\/" ( { b1 where b1 is Element of the carrier of A : b1 is_less_than rng C } ,A) is Element of the carrier of A

{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

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

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

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

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

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

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

{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

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

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

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

{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

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

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

rng C is set
C is Element of the carrier of f
O is set
C . O is set

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

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

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

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

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

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

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

rng C is set
C is Element of the carrier of f
O is set
C . O is set

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

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

"/\" ((rng C),f) is Element of the carrier of f
{ b1 where b1 is Element of the carrier of f : b1 is_less_than rng C } is set
"\/" ( { b1 where b1 is Element of the carrier of f : b1 is_less_than rng C } ,f) is Element of the carrier of f

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

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

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

C is set
O is set
C . C is set
C . O is set

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

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

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

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

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

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

C is set
O is set
C . C is set
C . O is set

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

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

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

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

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

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

(A,f,gg,c6) is Element of the carrier of A
(A,f,(gf "\/" g),c6) is Element of the carrier of A

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

(A,f,gg,c6) is Element of the carrier of A
(A,f,(gf "/\" g),c6) is Element of the carrier of A

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

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

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

rng c6 is set
C is Element of the carrier of A
C is set
c6 . C is set

(A,f,gf,O) is Element of the carrier of A
(A,f,gf,gg) is Element of the carrier of A
"\/" ((rng c6),A) is Element of the carrier of A
(A,f,gf,{}) is Element of the carrier of A

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

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

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

rng c6 is set
C is Element of the carrier of A
C is set
c6 . C is set

(A,f,g,O) is Element of the carrier of A
(A,f,g,gg) is Element of the carrier of A
"/\" ((rng c6),A) is Element of the carrier of A
{ b1 where b1 is Element of the carrier of A : b1 is_less_than rng c6 } is set
"\/" ( { b1 where b1 is Element of the carrier of A : b1 is_less_than rng c6 } ,A) is Element of the carrier of A
(A,f,g,{}) is Element of the carrier of A

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
{ b1 where b1 is Element of the carrier of A : b1 is_a_fixpoint_of f } is set
{ b1 where b1 is Element of the carrier of A : S1[b1] } is set
g is Element of the carrier of A
gg is Element of bool the carrier of A
c6 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

r is Element of the carrier of A

(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
c6 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

r is Element of the carrier of A

(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
c6 is non empty (A) (A) Element of bool the carrier of A

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

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

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

the carrier of (A,f) is non empty set
{ b1 where b1 is Element of the carrier of A : b1 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

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

the carrier of (A,f) is non empty set
{ b1 where b1 is Element of the carrier of A : b1 is_a_fixpoint_of f } is set
gf is set
g is Element of the carrier of A

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

the carrier of (A,f) is non empty set
gf is Element of the carrier of A
{ b1 where b1 is Element of the carrier of A : b1 is_a_fixpoint_of f } is set
g is Element of the carrier of A

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

the carrier of (A,f) is non empty set
bool the carrier of A is non empty set
{ b1 where b1 is Element of the carrier of A : b1 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
c6 is Element of the carrier of A
C is non empty (A) (A) Element of bool the carrier of A

C is Element of the carrier of A
C is Element of the carrier of A

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

the carrier of (A,f) is non empty set
c6 is set
c6 /\ the carrier of (A,f) is set
"\/" ((c6 /\ the carrier of (A,f)),A) is Element of the carrier of A
f . ("\/" ((c6 /\ 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

(A,f,("\/" ((c6 /\ 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)
{ b1 where b1 is Element of the carrier of A : b1 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)

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

(A,f,(),(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

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

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

(A,f,(),(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

(A,f,(),g) is Element of the carrier of A
A is non empty join-commutative