:: YELLOW_3 semantic presentation

K219() is Element of bool K215()

K215() is set

bool K215() is non empty set

K113() is set

bool K113() is non empty set

{} is empty Relation-like non-empty empty-yielding set

1 is non empty set

{{},1} is non empty set

bool K219() is non empty set

F

{ F

bool F

f is set

f is Element of F

c

F

f is RelStr

the carrier of f is set

bool the carrier of f is non empty set

f is empty Relation-like non-empty empty-yielding strongly_connected directed filtered Element of bool the carrier of f

downarrow f is Element of bool the carrier of f

c

y1 is Element of the carrier of f

C2 is Element of the carrier of f

uparrow f is Element of bool the carrier of f

c

y1 is Element of the carrier of f

C2 is Element of the carrier of f

f is set

f is set

[:f,f:] is Relation-like set

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

c

proj1 c

proj2 c

[:(proj1 c

y1 is set

C2 is set

q is set

[C2,q] is V1() set

{C2,q} is non empty set

{C2} is non empty set

{{C2,q},{C2}} is non empty set

f is set

f is set

c

[f,c

{f,c

{f} is non empty set

{{f,c

y1 is set

C2 is set

[y1,C2] is V1() set

{y1,C2} is non empty set

{y1} is non empty set

{{y1,C2},{y1}} is non empty set

[[f,c

{[f,c

{[f,c

{{[f,c

f `1 is set

(f `1) `1 is set

(f `1) `2 is set

f `2 is set

(f `2) `1 is set

(f `2) `2 is set

f is non empty transitive antisymmetric with_infima RelStr

the carrier of f is non empty set

f is Element of the carrier of f

y1 is Element of the carrier of f

c

C2 is Element of the carrier of f

f "/\" c

y1 "/\" C2 is Element of the carrier of f

{f,c

bool the carrier of f is non empty set

q is Element of the carrier of f

f is non empty transitive antisymmetric with_suprema RelStr

the carrier of f is non empty set

f is Element of the carrier of f

y1 is Element of the carrier of f

c

C2 is Element of the carrier of f

f "\/" c

y1 "\/" C2 is Element of the carrier of f

{y1,C2} is non empty Element of bool the carrier of f

bool the carrier of f is non empty set

q is Element of the carrier of f

f is non empty V55() reflexive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V158() up-complete /\-complete RelStr

the carrier of f is non empty set

bool the carrier of f is non empty set

f is Element of bool the carrier of f

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

c

("\/" (f,f)) "/\" c

f is non empty V55() reflexive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V158() up-complete /\-complete RelStr

the carrier of f is non empty set

bool the carrier of f is non empty set

f is Element of bool the carrier of f

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

c

("/\" (f,f)) "\/" c

f is RelStr

the carrier of f is set

bool the carrier of f is non empty set

f is Element of bool the carrier of f

c

downarrow f is Element of bool the carrier of f

downarrow c

y1 is set

C2 is Element of the carrier of f

q is Element of the carrier of f

f is RelStr

the carrier of f is set

bool the carrier of f is non empty set

f is Element of bool the carrier of f

c

uparrow f is Element of bool the carrier of f

uparrow c

y1 is set

C2 is Element of the carrier of f

q is Element of the carrier of f

f is non empty V55() reflexive transitive antisymmetric with_infima RelStr

the carrier of f is non empty set

f is non empty V55() reflexive transitive antisymmetric with_infima RelStr

the carrier of f is non empty set

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

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

c

y1 is Element of the carrier of f

C2 is Element of the carrier of f

{y1,C2} is non empty Element of bool the carrier of f

bool the carrier of f is non empty set

y1 "/\" C2 is Element of the carrier of f

c

c

c

(c

dom c

"/\" ({y1,C2},f) is Element of the carrier of f

c

c

bool the carrier of f is non empty set

"/\" ((c

{(c

"/\" ({(c

f is non empty V55() reflexive transitive antisymmetric with_suprema RelStr

the carrier of f is non empty set

f is non empty V55() reflexive transitive antisymmetric with_suprema RelStr

the carrier of f is non empty set

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

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

c

y1 is Element of the carrier of f

C2 is Element of the carrier of f

{y1,C2} is non empty Element of bool the carrier of f

bool the carrier of f is non empty set

y1 "\/" C2 is Element of the carrier of f

c

c

c

(c

dom c

"\/" ({y1,C2},f) is Element of the carrier of f

c

c

bool the carrier of f is non empty set

"\/" ((c

{(c

"\/" ({(c

F

the carrier of F

bool the carrier of F

{ b

union { b

"/\" ((union { b

{ ("/\" (b

"/\" ( { ("/\" (b

f is Element of the carrier of F

f is Element of bool the carrier of F

"/\" (f,F

F

the carrier of F

bool the carrier of F

{ ("/\" (b

"/\" ( { ("/\" (b

{ b

union { b

"/\" ((union { b

f is Element of the carrier of F

f is set

c

"/\" (c

F

the carrier of F

bool the carrier of F

{ ("\/" (b

"\/" ( { ("\/" (b

{ b

union { b

"\/" ((union { b

f is Element of the carrier of F

f is Element of bool the carrier of F

"\/" (f,F

F

the carrier of F

bool the carrier of F

{ ("\/" (b

"\/" ( { ("\/" (b

{ b

union { b

"\/" ((union { b

f is Element of the carrier of F

f is set

c

"\/" (c

f is Relation-like set

f is Relation-like set

proj1 f is set

proj1 f is set

[:(proj1 f),(proj1 f):] is Relation-like set

proj2 f is set

proj2 f is set

[:(proj2 f),(proj2 f):] is Relation-like set

c

y1 is set

C2 is set

[y1,C2] is V1() set

{y1,C2} is non empty set

{y1} is non empty set

{{y1,C2},{y1}} is non empty set

q is set

D1 is set

[q,D1] is V1() set

{q,D1} is non empty set

{q} is non empty set

{{q,D1},{q}} is non empty set

D9 is set

D2 is set

[D9,D2] is V1() set

{D9,D2} is non empty set

{D9} is non empty set

{{D9,D2},{D9}} is non empty set

[q,D9] is V1() set

{q,D9} is non empty set

{{q,D9},{q}} is non empty set

[D1,D2] is V1() set

{D1,D2} is non empty set

{D1} is non empty set

{{D1,D2},{D1}} is non empty set

D2 is set

D1 is set

[D2,D1] is V1() set

{D2,D1} is non empty set

{D2} is non empty set

{{D2,D1},{D2}} is non empty set

d is set

e is set

[d,e] is V1() set

{d,e} is non empty set

{d} is non empty set

{{d,e},{d}} is non empty set

[D2,d] is V1() set

{D2,d} is non empty set

{{D2,d},{D2}} is non empty set

[D1,e] is V1() set

{D1,e} is non empty set

{D1} is non empty set

{{D1,e},{D1}} is non empty set

q is set

D9 is set

[q,D9] is V1() set

{q,D9} is non empty set

{q} is non empty set

{{q,D9},{q}} is non empty set

D1 is set

D2 is set

[D1,D2] is V1() set

{D1,D2} is non empty set

{D1} is non empty set

{{D1,D2},{D1}} is non empty set

[q,D1] is V1() set

{q,D1} is non empty set

{{q,D1},{q}} is non empty set

[D9,D2] is V1() set

{D9,D2} is non empty set

{D9} is non empty set

{{D9,D2},{D9}} is non empty set

c

y1 is Relation-like set

f is Relation-like set

f is Relation-like set

(f,f) is Relation-like set

c

c

(c

c

(c

[((c

{((c

{((c

{{((c

(c

(c

[((c

{((c

{((c

{{((c

y1 is set

C2 is set

[y1,C2] is V1() set

{y1,C2} is non empty set

{y1} is non empty set

{{y1,C2},{y1}} is non empty set

q is set

D9 is set

[q,D9] is V1() set

{q,D9} is non empty set

{q} is non empty set

{{q,D9},{q}} is non empty set

D1 is set

D2 is set

[D1,D2] is V1() set

{D1,D2} is non empty set

{D1} is non empty set

{{D1,D2},{D1}} is non empty set

[q,D1] is V1() set

{q,D1} is non empty set

{{q,D1},{q}} is non empty set

[D9,D2] is V1() set

{D9,D2} is non empty set

{D9} is non empty set

{{D9,D2},{D9}} is non empty set

y1 is set

C2 is set

[y1,C2] is V1() set

{y1,C2} is non empty set

{y1} is non empty set

{{y1,C2},{y1}} is non empty set

y1 is set

C2 is set

[y1,C2] is V1() set

{y1,C2} is non empty set

{y1} is non empty set

{{y1,C2},{y1}} is non empty set

q is set

D9 is set

[q,D9] is V1() set

{q,D9} is non empty set

{q} is non empty set

{{q,D9},{q}} is non empty set

q is set

D9 is set

[q,D9] is V1() set

{q,D9} is non empty set

{q} is non empty set

{{q,D9},{q}} is non empty set

[y1,((c

{y1,((c

{{y1,((c

[y1,q] is V1() set

{y1,q} is non empty set

{{y1,q},{y1}} is non empty set

D1 is set

D2 is set

[D1,D2] is V1() set

{D1,D2} is non empty set

{D1} is non empty set

{{D1,D2},{D1}} is non empty set

D1 is set

D2 is set

[D1,D2] is V1() set

{D1,D2} is non empty set

{D1} is non empty set

{{D1,D2},{D1}} is non empty set

[C2,((c

{C2,((c

{C2} is non empty set

{{C2,((c

[C2,D9] is V1() set

{C2,D9} is non empty set

{{C2,D9},{C2}} is non empty set

f is set

f is set

[:f,f:] is Relation-like set

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

c

y1 is set

[:c

bool [:c

C2 is Relation-like f -defined f -valued Element of bool [:f,f:]

q is Relation-like c

(C2,q) is Relation-like set

[:f,c

[:f,y1:] is Relation-like set

[:[:f,c

bool [:[:f,c

D9 is set

D1 is set

D2 is set

[D1,D2] is V1() set

{D1,D2} is non empty set

{D1} is non empty set

{{D1,D2},{D1}} is non empty set

D9 `1 is set

(D9 `1) `2 is set

D9 `2 is set

(D9 `2) `2 is set

[((D9 `1) `2),((D9 `2) `2)] is V1() set

{((D9 `1) `2),((D9 `2) `2)} is non empty set

{((D9 `1) `2)} is non empty set

{{((D9 `1) `2),((D9 `2) `2)},{((D9 `1) `2)}} is non empty set

D2 is set

D1 is set

[D2,D1] is V1() set

{D2,D1} is non empty set

{D2} is non empty set

{{D2,D1},{D2}} is non empty set

d is set

e is set

[d,e] is V1() set

{d,e} is non empty set

{d} is non empty set

{{d,e},{d}} is non empty set

(D9 `1) `1 is set

(D9 `2) `1 is set

[((D9 `1) `1),((D9 `2) `1)] is V1() set

{((D9 `1) `1),((D9 `2) `1)} is non empty set

{((D9 `1) `1)} is non empty set

{{((D9 `1) `1),((D9 `2) `1)},{((D9 `1) `1)}} is non empty set

y is set

x is set

[y,x] is V1() set

{y,x} is non empty set

{y} is non empty set

{{y,x},{y}} is non empty set

y is set

e is set

[y,e] is V1() set

{y,e} is non empty set

{y} is non empty set

{{y,e},{y}} is non empty set

D2 `2 is set

D1 `2 is set

D2 `1 is set

D1 `1 is set

f is RelStr

the carrier of f is set

f is RelStr

the carrier of f is set

[: the carrier of f, the carrier of f:] is Relation-like set

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

[: the carrier of f, the carrier of f:] is Relation-like set

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

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

[: the carrier of f, the carrier of f:] is Relation-like set

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

( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]

[:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is Relation-like set

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

RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #) is strict RelStr

the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #) is set

the InternalRel of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #) is Relation-like the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #) -defined the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #) -valued Element of bool [: the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #), the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #):]

[: the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #), the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #):] is Relation-like set

bool [: the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #), the carrier of RelStr(# [: the carrier of f, the carrier of f:],( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) #):] is non empty set

c

the carrier of c

the InternalRel of c

[: the carrier of c

bool [: the carrier of c

y1 is strict RelStr

the carrier of y1 is set

the InternalRel of y1 is Relation-like the carrier of y1 -defined the carrier of y1 -valued Element of bool [: the carrier of y1, the carrier of y1:]

[: the carrier of y1, the carrier of y1:] is Relation-like set

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

f is RelStr

f is RelStr

(f,f) is strict RelStr

the carrier of (f,f) is set

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

c

proj1 c

the carrier of f is set

bool the carrier of f is non empty set

y1 is set

the carrier of f is set

[: the carrier of f, the carrier of f:] is Relation-like set

C2 is set

[y1,C2] is V1() set

{y1,C2} is non empty set

{y1} is non empty set

{{y1,C2},{y1}} is non empty set

proj2 c

the carrier of f is set

bool the carrier of f is non empty set

y1 is set

[: the carrier of f, the carrier of f:] is Relation-like set

C2 is set

[C2,y1] is V1() set

{C2,y1} is non empty set

{C2} is non empty set

{{C2,y1},{C2}} is non empty set

f is RelStr

the carrier of f is set

bool the carrier of f is non empty set

f is RelStr

the carrier of f is set

bool the carrier of f is non empty set

c

y1 is Element of bool the carrier of f

[:c

(f,f) is strict RelStr

the carrier of (f,f) is set

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

[:c

[: the carrier of f, the carrier of f:] is Relation-like set

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

f is non empty RelStr

the carrier of f is non empty set

f is non empty RelStr

the carrier of f is non empty set

c

y1 is Element of the carrier of f

[c

{c

{c

{{c

(f,f) is strict RelStr

the carrier of (f,f) is set

q is Element of the carrier of f

C2 is Element of the carrier of f

[q,C2] is V1() Element of [: the carrier of f, the carrier of f:]

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

{q,C2} is non empty set

{q} is non empty set

{{q,C2},{q}} is non empty set

f is non empty RelStr

f is non empty RelStr

(f,f) is strict RelStr

the carrier of (f,f) is set

c

c

the carrier of f is non empty set

the carrier of f is non empty set

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

c

the carrier of f is non empty set

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

f is non empty RelStr

the carrier of f is non empty set

f is non empty RelStr

the carrier of f is non empty set

(f,f) is strict RelStr

c

y1 is Element of the carrier of f

C2 is Element of the carrier of f

q is Element of the carrier of f

(f,f,c

the carrier of (f,f) is set

{c

{c

{{c

(f,f,y1,q) is V1() Element of the carrier of (f,f)

{y1,q} is non empty set

{y1} is non empty set

{{y1,q},{y1}} is non empty set

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

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

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

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

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

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

[(f,f,c

{(f,f,c

{(f,f,c

{{(f,f,c

[(f,f,c

([(f,f,c

[(f,f,c

([(f,f,c

([(f,f,c

([(f,f,c

[(([(f,f,c

{(([(f,f,c

{(([(f,f,c

{{(([(f,f,c

[(([(f,f,c

{(([(f,f,c

{(([(f,f,c

{{(([(f,f,c

( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]

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

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

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

the InternalRel of (f,f) is Relation-like the carrier of (f,f) -defined the carrier of (f,f) -valued Element of bool [: the carrier of (f,f), the carrier of (f,f):]

[: the carrier of (f,f), the carrier of (f,f):] is Relation-like set

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

the InternalRel of (f,f) is Relation-like the carrier of (f,f) -defined the carrier of (f,f) -valued Element of bool [: the carrier of (f,f), the carrier of (f,f):]

[: the carrier of (f,f), the carrier of (f,f):] is Relation-like set

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

( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]

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

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

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

(f,f,c

(f,f) is strict RelStr

the carrier of (f,f) is set

{c

{{c

(f,f,C2,q) is V1() Element of the carrier of (f,f)

(f,f) is strict RelStr

the carrier of (f,f) is set

{C2,q} is non empty set

{C2} is non empty set

{{C2,q},{C2}} is non empty set

f is non empty RelStr

f is non empty RelStr

(f,f) is strict RelStr

the carrier of (f,f) is set

c

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

(f,f,c

the carrier of f is non empty set

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

(f,f,c

the carrier of f is non empty set

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

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

(f,f,(f,f,y1),(f,f,y1)) is V1() Element of the carrier of (f,f)

{(f,f,y1),(f,f,y1)} is non empty set

{(f,f,y1)} is non empty set

{{(f,f,y1),(f,f,y1)},{(f,f,y1)}} is non empty set

C2 is set

q is set

[C2,q] is V1() set

{C2,q} is non empty set

{C2} is non empty set

{{C2,q},{C2}} is non empty set

(f,f,(f,f,c

{(f,f,c

{(f,f,c

{{(f,f,c

C2 is set

q is set

[C2,q] is V1() set

{C2,q} is non empty set

{C2} is non empty set

{{C2,q},{C2}} is non empty set

f is RelStr

f is RelStr

(f,f) is strict RelStr

the carrier of (f,f) is set

the carrier of f is set

the carrier of f is set

c

the carrier of c

[: the carrier of (f,f), the carrier of c

bool [: the carrier of (f,f), the carrier of c

y1 is Relation-like the carrier of (f,f) -defined the carrier of c

C2 is Relation-like the carrier of (f,f) -defined the carrier of c

q is set

D9 is set

y1 . (q,D9) is set

C2 . (q,D9) is set

[: the carrier of f, the carrier of f:] is Relation-like set

f is non empty RelStr

f is non empty RelStr

(f,f) is strict RelStr

the carrier of f is non empty set

the Element of the carrier of f is Element of the carrier of f

the carrier of f is non empty set

the Element of the carrier of f is Element of the carrier of f

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

the carrier of (f,f) is set

{ the Element of the carrier of f, the Element of the carrier of f} is non empty set

{ the Element of the carrier of f} is non empty set

{{ the Element of the carrier of f, the Element of the carrier of f},{ the Element of the carrier of f}} is non empty set

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

f is V55() reflexive RelStr

f is V55() reflexive RelStr

(f,f) is strict RelStr

c

the carrier of (f,f) is set

[c

{c

{c

{{c

the InternalRel of (f,f) is Relation-like the carrier of (f,f) -defined the carrier of (f,f) -valued Element of bool [: the carrier of (f,f), the carrier of (f,f):]

[: the carrier of (f,f), the carrier of (f,f):] is Relation-like set

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

the carrier of f is set

the carrier of f is set

[: the carrier of f, the carrier of f:] is Relation-like set

y1 is set

C2 is set

[y1,C2] is V1() set

{y1,C2} is non empty set

{y1} is non empty set

{{y1,C2},{y1}} is non empty set

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued V17( the carrier of f) reflexive Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is Relation-like set

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

[y1,y1] is V1() set

{y1,y1} is non empty set

{{y1,y1},{y1}} is non empty set

the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued V17( the carrier of f) reflexive Element of bool [: the carrier of f, the carrier of f:]

[: the carrier of f, the carrier of f:] is Relation-like set

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

[C2,C2] is V1() set

{C2,C2} is non empty set

{C2} is non empty set

{{C2,C2},{C2}} is non empty set

[[y1,C2],[y1,C2]] is V1() set

{[y1,C2],[y1,C2]} is non empty Relation-like set

{[y1,C2]} is non empty Relation-like set

{{[y1,C2],[y1,C2]},{[y1,C2]}} is non empty set

[[y1,C2],[y1,C2]] `1 is set

[[y1,C2],[y1,C2]] `2 is set

([[y1,C2],[y1,C2]] `1) `1 is set

([[y1,C2],[y1,C2]] `1) `2 is set

( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]

[:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is Relation-like set

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

f is antisymmetric RelStr

f is antisymmetric RelStr

(f,f) is strict RelStr

c

the carrier of (f,f) is set

y1 is set

[c

{c

{c

{{c

the InternalRel of (f,f) is Relation-like the carrier of (f,f) -defined the carrier of (f,f) -valued Element of bool [: the carrier of (f,f), the carrier of (f,f):]

[: the carrier of (f,f), the carrier of (f,f):] is Relation-like set

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

[y1,c

{y1,c

{y1} is non empty set

{{y1,c

the carrier of f is set

the carrier of f is set

[: the carrier of f, the carrier of f:] is Relation-like set

C2 is set

q is set

[C2,q] is V1() set

{C2,q} is non empty set

{C2} is non empty set

{{C2,q},{C2}} is non empty set

D9 is set

D1 is set

[D9,D1] is V1() set

{D9,D1} is non empty set

{D9} is non empty set

{{D9,D1},{D9}} is non empty set

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

[: the carrier of f, the carrier of f:] is Relation-like set

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

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

[: the carrier of f, the carrier of f:] is Relation-like set

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

( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]

[:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is Relation-like set

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

[y1,c

([y1,c

[y1,c

([y1,c

[(([y1,c

{(([y1,c

{(([y1,c

{{(([y1,c

y1 `1 is set

[(y1 `1),(([y1,c

{(y1 `1),(([y1,c

{(y1 `1)} is non empty set

{{(y1 `1),(([y1,c

c

[(y1 `1),(c

{(y1 `1),(c

{{(y1 `1),(c

[C2,q] `1 is set

[D9,([C2,q] `1)] is V1() set

{D9,([C2,q] `1)} is non empty set

{{D9,([C2,q] `1)},{D9}} is non empty set

[D9,C2] is V1() set

{D9,C2} is non empty set

{{D9,C2},{D9}} is non empty set

([y1,c

([y1,c

[(([y1,c

{(([y1,c

{(([y1,c

{{(([y1,c

y1 `2 is set

[(y1 `2),(([y1,c

{(y1 `2),(([y1,c

{(y1 `2)} is non empty set

{{(y1 `2),(([y1,c

c

[(y1 `2),(c

{(y1 `2),(c

{{(y1 `2),(c

[C2,q] `2 is set

[D1,([C2,q] `2)] is V1() set

{D1,([C2,q] `2)} is non empty set

{D1} is non empty set

{{D1,([C2,q] `2)},{D1}} is non empty set

[D1,q] is V1() set

{D1,q} is non empty set

{{D1,q},{D1}} is non empty set

[c

([c

[c

([c

[(([c

{(([c

{(([c

{{(([c

[(c

{(c

{(c

{{(c

[(c

{(c

{{(c

[D9,D1] `2 is set

[q,([D9,D1] `2)] is V1() set

{q,([D9,D1] `2)} is non empty set

{q} is non empty set

{{q,([D9,D1] `2)},{q}} is non empty set

[q,D1] is V1() set

{q,D1} is non empty set

{{q,D1},{q}} is non empty set

([c

([c

[(([c

{(([c

{(([c

{{(([c

[(c

{(c

{(c

{{(c

[(c

{(c

{{(c

[D9,D1] `1 is set

[C2,([D9,D1] `1)] is V1() set

{C2,([D9,D1] `1)} is non empty set

{{C2,([D9,D1] `1)},{C2}} is non empty set

[C2,D9] is V1() set

{C2,D9} is non empty set

{{C2,D9},{C2}} is non empty set

f is transitive RelStr

f is transitive RelStr

(f,f) is strict RelStr

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

the carrier of f is set

[: the carrier of f, the carrier of f:] is Relation-like set

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

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

the carrier of f is set

[: the carrier of f, the carrier of f:] is Relation-like set

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

C2 is set

the carrier of (f,f) is set

q is set

D9 is set

[C2,q] is V1() set

{C2,q} is non empty set

{C2} is non empty set

{{C2,q},{C2}} is non empty set

the InternalRel of (f,f) is Relation-like the carrier of (f,f) -defined the carrier of (f,f) -valued Element of bool [: the carrier of (f,f), the carrier of (f,f):]

[: the carrier of (f,f), the carrier of (f,f):] is Relation-like set

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

[q,D9] is V1() set

{q,D9} is non empty set

{q} is non empty set

{{q,D9},{q}} is non empty set

[C2,D9] is V1() set

{C2,D9} is non empty set

{{C2,D9},{C2}} is non empty set

[: the carrier of f, the carrier of f:] is Relation-like set

D1 is set

D2 is set

[D1,D2] is V1() set

{D1,D2} is non empty set

{D1} is non empty set

{{D1,D2},{D1}} is non empty set

D2 is set

D1 is set

[D2,D1] is V1() set

{D2,D1} is non empty set

{D2} is non empty set

{{D2,D1},{D2}} is non empty set

( the carrier of f, the carrier of f, the carrier of f, the carrier of f, the InternalRel of f, the InternalRel of f) is Relation-like [: the carrier of f, the carrier of f:] -defined [: the carrier of f, the carrier of f:] -valued Element of bool [:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:]

[:[: the carrier of f, the carrier of f:],[: the carrier of f, the carrier of f:]:] is Relation-like set

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

[q,D9] `1 is set

([q,D9] `1) `1 is set

[q,D9] `2 is set

([q,D9] `2) `1 is set

[(([q,D9] `1) `1),(([q,D9] `2) `1)] is V1() set

{(([q,D9] `1) `1),(([q,D9] `2) `1)} is non empty set

{(([q,D9] `1) `1)} is non empty set

{{(([q,D9] `1) `1),(([q,D9] `2) `1)},{(([q,D9] `1) `1)}} is non empty set

q `1 is set

[(q `1),(([q,D9] `2) `1)] is V1() set

{(q `1),(([q,D9] `2) `1)} is non empty set

{(q `1)} is non empty set

{{(q `1),(([q,D9] `2) `1)},{(q `1)}} is non empty set

D9 `1 is set

[(q `1),(D9 `1)] is V1() set

{(q `1),(D9 `1)} is non empty set

{{(q `1),(D9 `1)},{(q `1)}} is non empty set

[D1,(D9 `1)] is V1() set

{D1,(D9 `1)} is non empty set

{{D1,(D9 `1)},{D1}} is non empty set

[D1,D2] is V1() set

{D1,D2} is non empty set

{{D1,D2},{D1}} is non empty set

d is set

e is set

[d,e] is V1() set

{d,e} is non empty set

{d} is non empty set

{{d,e},{d}} is non empty set

[C2,q] `1 is set

([C2,q] `1) `1 is set

[C2,q] `2 is set

([C2,q] `2) `1 is set

[(([C2,q] `1) `1),(([C2,q] `2) `1)] is V1() set

{(([C2,q] `1) `1),(([C2,q] `2) `1)} is non empty set

{(([C2,q] `1) `1)} is non empty set

{{(([C2,q] `1) `1),(([C2,q] `2) `1)},{(([C2,q] `1) `1)}} is non empty set

C2 `1 is set

[(C2 `1),(([C2,q] `2) `1)] is V1() set

{(C2 `1),(([C2,q] `2) `1)} is non empty set

{(C2 `1)} is non empty set

{{(C2 `1),(([C2,q] `2) `1)},{(C2 `1)}} is non empty set

[(C2 `1),(q `1)] is V1() set

{(C2 `1),(q `1)} is non empty set

{{(C2 `1),(q `1)},{(C2 `1)}} is non empty set

[d,(q `1)] is V1() set

{d,(q `1)} is non empty set

{{d,(q `1)},{d}} is non empty set

[d,D1] is V1() set

{d,D1} is non empty set

{{d,D1},{d}} is non empty set

[d,D2] is V1() set

{d,D2} is non empty set

{{d,D2},{d}} is non empty set

[d,(D9 `1)] is V1() set

{d,(D9 `1)} is non empty set

{{d,(D9 `1)},{d}} is non empty set

[(C2 `1),(D9 `1)] is V1() set

{(C2 `1),(D9 `1)} is non empty set

{{(C2 `1),(D9 `1)},{(C2 `1)}} is non empty set

([q,D9] `1) `2 is set

([q,D9] `2) `2 is set

[(([q,D9] `1) `2),(([q,D9] `2) `2)] is V1() set

{(([q,D9] `1) `2),(([q,D9] `2) `2)} is non empty set

{(([q,D9] `1) `2)} is non empty set

{{(([q,D9] `1) `2),(([q,D9] `2) `2)},{(([q,D9] `1) `2)}} is non empty set

q `2 is set

[(q `2),(([q,D9] `2) `2)] is V1() set

{(q `2),(([q,D9] `2) `2)} is non empty set

{(q `2)} is non empty set

{{(q `2),(([q,D9] `2) `2)},{(q `2)}} is non empty set

D9 `2 is set

[(q `2),(D9 `2)] is V1() set

{(q `2),(D9 `2)} is non empty set

{{(q `2),(D9 `2)},{(q `2)}} is non empty set

[D2,(D9 `2)] is V1() set

{D2,(D9 `2)} is non empty set

{D2} is non empty set

{{D2,(D9 `2)},{D2}} is non empty set

[D2,D1] is V1() set

{D2,D1} is non empty set

{{D2,D1},{D2}} is non empty set

([C2,q] `1) `2 is set

([C2,q] `2) `2 is set

[(([C2,q] `1) `2),(([C2,q] `2) `2)] is V1() set

{(([C2,q] `1) `2),(([C2,q] `2) `2)} is non empty set

{(([C2,q] `1) `2)} is non empty set

{{(([C2,q] `1) `2),(([C2,q] `2) `2)},{(([C2,q] `1) `2)}} is non empty set

C2 `2 is set

[(C2 `2),(([C2,q] `2) `2)] is V1() set

{(C2 `2),(([C2,q] `2) `2)} is non empty set

{(C2 `2)} is non empty set

{{(C2 `2),(([C2,q] `2) `2)},{(C2 `2)}} is non empty set

[(C2 `2),(q `2)] is V1() set

{(C2 `2),(q `2)} is non empty set

{{(C2 `2),(q `2)},{(C2 `2)}} is non empty set

[e,(q `2)] is V1() set

{e,(q `2)} is non empty set

{e} is non empty set

{{e,(q `2)},{e}} is non empty set

[e,D2] is V1() set

{e,D2} is non empty set

{{e,D2},{e}} is non empty set

[e,D1] is V1() set

{e,D1} is non empty set

{{e,D1},{e}} is non empty set

[e,(D9 `2)] is V1() set

{e,(D9 `2)} is non empty set

{{e,(D9 `2)},{e}} is non empty set

[(C2 `2),(D9 `2)] is V1() set

{(C2 `2),(D9 `2)} is non empty set

{{(C2 `2),(D9 `2)},{(C2 `2)}} is non empty set

[C2,D9] `1 is set

[C2,D9] `2 is set

f is non empty with_suprema RelStr

f is non empty with_suprema RelStr

(f,f) is non empty strict RelStr

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

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

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

the carrier of f is non empty set

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

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

q is Element of the carrier of f

the carrier of f is non empty set

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

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

D9 is Element of the carrier of f

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

(f,f,q,D9) is V1() Element of the carrier of (f,f)

{q,D9} is non empty set

{q} is non empty set

{{q,D9},{q}} is non empty set

D1 is V1() Element of the carrier of (f,f)

(f,f,(f,f,y1),(f,f,y1)) is V1() Element of the carrier of (f,f)

{(f,f,y1),(f,f,y1)} is non empty set

{(f,f,y1)} is non empty set

{{(f,f,y1),(f,f,y1)},{(f,f,y1)}} is non empty set

(f,f,(f,f,C2),(f,f,C2)) is V1() Element of the carrier of (f,f)

{(f,f,C2),(f,f,C2)} is non empty set

{(f,f,C2)} is non empty set

{{(f,f,C2),(f,f,C2)},{(f,f,C2)}} is non empty set

D2 is set

D2 is set

[D2,D2] is V1() set

{D2,D2} is non empty set

{D2} is non empty set

{{D2,D2},{D2}} is non empty set

D1 is set

d is set

[D1,d] is V1() set

{D1,d} is non empty set

{D1} is non empty set

{{D1,d},{D1}} is non empty set

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

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

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

(f,f,(f,f,D2),(f,f,D2)) is V1() Element of the carrier of (f,f)

{(f,f,D2),(f,f,D2)} is non empty set

{(f,f,D2)} is non empty set

{{(f,f,D2),(f,f,D2)},{(f,f,D2)}} is non empty set

D2 is set

D1 is set

[D2,D1] is V1() set

{D2,D1} is non empty set

{D2} is non empty set

{{D2,D1},{D2}} is non empty set

f is non empty with_infima RelStr

f is non empty with_infima RelStr

(f,f) is non empty strict RelStr

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

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

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

the carrier of f is non empty set

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

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

q is Element of the carrier of f

the carrier of f is non empty set

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

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

D9 is Element of the carrier of f

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

(f,f,q,D9) is V1() Element of the carrier of (f,f)

{q,D9} is non empty set

{q} is non empty set

{{q,D9},{q}} is non empty set

D1 is V1() Element of the carrier of (f,f)

(f,f,(f,f,y1),(f,f,y1)) is V1() Element of the carrier of (f,f)

{(f,f,y1),(f,f,y1)} is non empty set

{(f,f,y1)} is non empty set

{{(f,f,y1),(f,f,y1)},{(f,f,y1)}} is non empty set

(f,f,(f,f,C2),(f,f,C2)) is V1() Element of the carrier of (f,f)

{(f,f,C2),(f,f,C2)} is non empty set

{(f,f,C2)} is non empty set

{{(f,f,C2),(f,f,C2)},{(f,f,C2)}} is non empty set

D2 is set

D2 is set

[D2,D2] is V1() set

{D2,D2} is non empty set

{D2} is non empty set

{{D2,D2},{D2}} is non empty set

D1 is set

d is set

[D1,d] is V1() set

{D1,d} is non empty set

{D1} is non empty set

{{D1,d},{D1}} is non empty set

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

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

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

(f,f,(f,f,D2),(f,f,D2)) is V1() Element of the carrier of (f,f)

{(f,f,D2),(f,f,D2)} is non empty set

{(f,f,D2)} is non empty set

{{(f,f,D2),(f,f,D2)},{(f,f,D2)}} is non empty set

D2 is set

D1 is set

[D2,D1] is V1() set

{D2,D1} is non empty set

{D2} is non empty set

{{D2,D1},{D2}} is non empty set

f is RelStr

f is RelStr

(f,f) is strict RelStr

the carrier of (f,f) is set

the carrier of f is set

the carrier of f is set

[: the carrier of f, the carrier of f:] is Relation-like set

c

f is non empty RelStr

f is non empty RelStr

(f,f) is non empty strict RelStr

the carrier of f is non empty set

the carrier of f is non empty set

the Element of the carrier of f is Element of the carrier of f

y1 is Element of the carrier of f

(f,f,y1, the Element of the carrier of f) is V1() Element of the carrier of (f,f)

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

{y1, the Element of the carrier of f} is non empty set

{y1} is non empty set

{{y1, the Element of the carrier of f},{y1}} is non empty set

the carrier of f is non empty set

the Element of the carrier of f is Element of the carrier of f

y1 is Element of the carrier of f

(f,f, the Element of the carrier of f,y1) is V1() Element of the carrier of (f,f)

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

{ the Element of the carrier of f,y1} is non empty set

{ the Element of the carrier of f} is non empty set

{{ the Element of the carrier of f,y1},{ the Element of the carrier of f}} is non empty set

f is non empty V55() reflexive RelStr

f is non empty V55() reflexive RelStr

(f,f) is non empty strict V55() reflexive RelStr

the carrier of f is non empty set

the carrier of f is non empty set

the Element of the carrier of f is Element of the carrier of f

y1 is Element of the carrier of f

C2 is Element of the carrier of f

(f,f,y1, the Element of the carrier of f) is V1() Element of the carrier of (f,f)

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

{y1, the Element of the carrier of f} is non empty set

{y1} is non empty set

{{y1, the Element of the carrier of f},{y1}} is non empty set

(f,f,C2, the Element of the carrier of f) is V1() Element of the carrier of (f,f)

{C2, the Element of the carrier of f} is non empty set

{C2} is non empty set

{{C2, the Element of the carrier of f},{C2}} is non empty set

the carrier of f is non empty set

the Element of the carrier of f is Element of the carrier of f

y1 is Element of the carrier of f

C2 is Element of the carrier of f

(f,f, the Element of the carrier of f,y1) is V1() Element of the carrier of (f,f)

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

{ the Element of the carrier of f,y1} is non empty set

{ the Element of the carrier of f} is non empty set

{{ the Element of the carrier of f,y1},{ the Element of the carrier of f}} is non empty set

(f,f, the Element of the carrier of f,C2) is V1() Element of the carrier of (f,f)

{ the Element of the carrier of f,C2} is non empty set

{{ the Element of the carrier of f,C2},{ the Element of the carrier of f}} is non empty set

f is non empty V55() reflexive RelStr

f is non empty V55() reflexive RelStr

(f,f) is non empty strict V55() reflexive RelStr

the carrier of f is non empty set

the carrier of f is non empty set

the Element of the carrier of f is Element of the carrier of f

y1 is Element of the carrier of f

C2 is Element of the carrier of f

q is Element of the carrier of f

(f,f,y1, the Element of the carrier of f) is V1() Element of the carrier of (f,f)

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

{y1, the Element of the carrier of f} is non empty set

{y1} is non empty set

{{y1, the Element of the carrier of f},{y1}} is non empty set

(f,f,C2, the Element of the carrier of f) is V1() Element of the carrier of (f,f)

{C2, the Element of the carrier of f} is non empty set

{C2} is non empty set

{{C2, the Element of the carrier of f},{C2}} is non empty set

(f,f,q, the Element of the carrier of f) is V1() Element of the carrier of (f,f)

{q, the Element of the carrier of f} is non empty set

{q} is non empty set

{{q, the Element of the carrier of f},{q}} is non empty set

the carrier of f is non empty set

the Element of the carrier of f is Element of the carrier of f

y1 is Element of the carrier of f

C2 is Element of the carrier of f

q is Element of the carrier of f

(f,f, the Element of the carrier of f,y1) is V1() Element of the carrier of (f,f)

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

{ the Element of the carrier of f,y1} is non empty set

{ the Element of the carrier of f} is non empty set

{{ the Element of the carrier of f,y1},{ the Element of the carrier of f}} is non empty set

(f,f, the Element of the carrier of f,C2) is V1() Element of the carrier of (f,f)

{ the Element of the carrier of f,C2} is non empty set

{{ the Element of the carrier of f,C2},{ the Element of the carrier of f}} is non empty set

(f,f, the Element of the carrier of f,q) is V1() Element of the carrier of (f,f)

{ the Element of the carrier of f,q} is non empty set

{{ the Element of the carrier of f,q},{ the Element of the carrier of f}} is non empty set

f is non empty V55() reflexive RelStr

f is non empty V55() reflexive RelStr

(f,f) is non empty strict V55() reflexive RelStr

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

the carrier of f is non empty set

the carrier of f is non empty set

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

c

y1 is Element of the carrier of f

the Element of the carrier of f is Element of the carrier of f

(f,f,c

{c