:: CONLAT_1 semantic presentation

K118() is set

bool K118() is non empty set

{} is empty set

1 is non empty set

{{}} is non empty set

2-sorted(# {{}},{{}} #) is strict 2-sorted

{{}} is non empty set

2-sorted(# {{}},{{}} #) is strict 2-sorted

2-sorted(# {},{} #) is strict 2-sorted

{{}} is non empty set

[:{{}},{{}}:] is non empty set

bool [:{{}},{{}}:] is non empty set

the Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:] is Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:]

({{}},{{}}, the Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:]) is () ()

{{}} is non empty set

[:{{}},{{}}:] is non empty set

bool [:{{}},{{}}:] is non empty set

the Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:] is Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:]

({{}},{{}}, the Relation-like {{}} -defined {{}} -valued Element of bool [:{{}},{{}}:]) is () ()

C is () 2-sorted

the carrier' of C is set

the carrier of C is set

C is () 2-sorted

the carrier of C is non empty set

bool the carrier of C is non empty set

the carrier' of C is non empty set

bool the carrier' of C is non empty set

C is () ()

the carrier of C is non empty set

the carrier' of C is non empty set

C is () ()

the carrier of C is non empty set

the carrier' of C is non empty set

C is () ()

the carrier of C is non empty set

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

the carrier' of C is non empty set

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

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

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

{ [b

( not b

X is set

ExX is Element of bool the carrier of C

{ b

( not b

[ExX, { b

( not b

{ExX, { b

( not b

{ExX} is non empty set

{{ExX, { b

( not b

X is Relation-like set

ExX is set

ExX is set

[ExX,ExX] is V15() set

{ExX,ExX} is non empty set

{ExX} is non empty set

{{ExX,ExX},{ExX}} is non empty set

E1 is set

[ExX,E1] is V15() set

{ExX,E1} is non empty set

{{ExX,E1},{ExX}} is non empty set

O is Element of bool the carrier of C

{ b

( not b

[O, { b

( not b

{O, { b

( not b

{O} is non empty set

{{O, { b

( not b

[ExX,ExX] `2 is set

[O, { b

( not b

InX is Element of bool the carrier of C

{ b

( not b

[InX, { b

( not b

{InX, { b

( not b

{InX} is non empty set

{{InX, { b

( not b

[ExX,E1] `2 is set

[InX, { b

( not b

[O, { b

( not b

[ExX,ExX] `1 is set

[ExX,E1] `1 is set

[InX, { b

( not b

ExX is Relation-like Function-like set

proj1 ExX is set

ExX is set

E1 is set

[ExX,E1] is V15() set

{ExX,E1} is non empty set

{ExX} is non empty set

{{ExX,E1},{ExX}} is non empty set

O is Element of bool the carrier of C

{ b

( not b

[O, { b

( not b

{O, { b

( not b

{O} is non empty set

{{O, { b

( not b

[ExX,E1] `1 is set

[O, { b

( not b

ExX is set

E1 is Element of bool the carrier of C

{ b

( not b

[E1, { b

( not b

{E1, { b

( not b

{E1} is non empty set

{{E1, { b

( not b

proj2 ExX is set

ExX is set

E1 is set

[E1,ExX] is V15() set

{E1,ExX} is non empty set

{E1} is non empty set

{{E1,ExX},{E1}} is non empty set

O is Element of bool the carrier of C

{ b

( not b

[O, { b

( not b

{O, { b

( not b

{O} is non empty set

{{O, { b

( not b

InX is set

In is Element of the carrier' of C

[E1,ExX] `2 is set

[O, { b

( not b

ExX is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

E1 is Element of bool the carrier of C

ExX . E1 is Element of bool the carrier' of C

{ b

( not b

O is set

[E1,O] is V15() set

{E1,O} is non empty set

{E1} is non empty set

{{E1,O},{E1}} is non empty set

InX is Element of bool the carrier of C

{ b

( not b

[InX, { b

( not b

{InX, { b

( not b

{InX} is non empty set

{{InX, { b

( not b

[E1,O] `2 is set

[InX, { b

( not b

[E1,O] `1 is set

[InX, { b

( not b

E1 is Element of bool the carrier of C

ExX . E1 is Element of bool the carrier' of C

{ b

( not b

X is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

X is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

ExX is set

X . ExX is set

X . ExX is set

ExX is Element of bool the carrier of C

X . ExX is Element of bool the carrier' of C

{ b

( not b

X . ExX is Element of bool the carrier' of C

dom X is Element of bool (bool the carrier of C)

bool (bool the carrier of C) is non empty set

dom X is Element of bool (bool the carrier of C)

C is () ()

the carrier' of C is non empty set

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

the carrier of C is non empty set

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

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

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

{ [b

( not b

X is set

ExX is Element of bool the carrier' of C

{ b

( not b

[ExX, { b

( not b

{ExX, { b

( not b

{ExX} is non empty set

{{ExX, { b

( not b

X is Relation-like set

ExX is set

ExX is set

[ExX,ExX] is V15() set

{ExX,ExX} is non empty set

{ExX} is non empty set

{{ExX,ExX},{ExX}} is non empty set

E1 is set

[ExX,E1] is V15() set

{ExX,E1} is non empty set

{{ExX,E1},{ExX}} is non empty set

O is Element of bool the carrier' of C

{ b

( not b

[O, { b

( not b

{O, { b

( not b

{O} is non empty set

{{O, { b

( not b

[ExX,ExX] `2 is set

[O, { b

( not b

InX is Element of bool the carrier' of C

{ b

( not b

[InX, { b

( not b

{InX, { b

( not b

{InX} is non empty set

{{InX, { b

( not b

[ExX,E1] `2 is set

[InX, { b

( not b

[O, { b

( not b

[ExX,ExX] `1 is set

[ExX,E1] `1 is set

[InX, { b

( not b

ExX is Relation-like Function-like set

proj1 ExX is set

ExX is set

E1 is set

[ExX,E1] is V15() set

{ExX,E1} is non empty set

{ExX} is non empty set

{{ExX,E1},{ExX}} is non empty set

O is Element of bool the carrier' of C

{ b

( not b

[O, { b

( not b

{O, { b

( not b

{O} is non empty set

{{O, { b

( not b

[ExX,E1] `1 is set

[O, { b

( not b

ExX is set

E1 is Element of bool the carrier' of C

{ b

( not b

[E1, { b

( not b

{E1, { b

( not b

{E1} is non empty set

{{E1, { b

( not b

proj2 ExX is set

ExX is set

E1 is set

[E1,ExX] is V15() set

{E1,ExX} is non empty set

{E1} is non empty set

{{E1,ExX},{E1}} is non empty set

O is Element of bool the carrier' of C

{ b

( not b

[O, { b

( not b

{O, { b

( not b

{O} is non empty set

{{O, { b

( not b

InX is set

In is Element of the carrier of C

[E1,ExX] `2 is set

[O, { b

( not b

ExX is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

E1 is Element of bool the carrier' of C

ExX . E1 is Element of bool the carrier of C

{ b

( not b

O is set

[E1,O] is V15() set

{E1,O} is non empty set

{E1} is non empty set

{{E1,O},{E1}} is non empty set

InX is Element of bool the carrier' of C

{ b

( not b

[InX, { b

( not b

{InX, { b

( not b

{InX} is non empty set

{{InX, { b

( not b

[E1,O] `2 is set

[InX, { b

( not b

[E1,O] `1 is set

[InX, { b

( not b

E1 is Element of bool the carrier' of C

ExX . E1 is Element of bool the carrier of C

{ b

( not b

X is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

X is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

ExX is set

X . ExX is set

X . ExX is set

ExX is Element of bool the carrier' of C

X . ExX is Element of bool the carrier of C

{ b

( not b

X . ExX is Element of bool the carrier of C

dom X is Element of bool (bool the carrier' of C)

bool (bool the carrier' of C) is non empty set

dom X is Element of bool (bool the carrier' of C)

C is () ()

the carrier of C is non empty set

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

the carrier' of C is non empty set

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

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

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

X is Element of the carrier of C

{X} is non empty set

(C) . {X} is set

{ b

X is set

X is Element of bool the carrier of C

{ b

( not b

the Element of X is Element of X

ExX is set

E1 is Element of the carrier of C

InX is Element of the carrier' of C

O is Element of the carrier' of C

InX is Element of the carrier' of C

ExX is set

E1 is Element of the carrier' of C

ExX is Element of the carrier' of C

E1 is Element of the carrier of C

O is Element of the carrier' of C

(C) . X is Element of bool the carrier' of C

C is () ()

the carrier' of C is non empty set

(C) is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

the carrier of C is non empty set

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

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

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

X is Element of the carrier' of C

{X} is non empty set

(C) . {X} is set

{ b

X is set

X is Element of bool the carrier' of C

{ b

( not b

the Element of X is Element of X

ExX is set

E1 is Element of the carrier' of C

InX is Element of the carrier of C

O is Element of the carrier of C

InX is Element of the carrier of C

ExX is set

E1 is Element of the carrier of C

ExX is Element of the carrier of C

E1 is Element of the carrier' of C

O is Element of the carrier of C

(C) . X is Element of bool the carrier of C

C is () ()

the carrier of C is non empty set

bool the carrier of C is non empty set

the carrier' of C is non empty set

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

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

bool (bool the carrier of C) is non empty set

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

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

X is Element of bool the carrier of C

X is Element of bool the carrier of C

(C) . X is Element of bool the carrier' of C

(C) . X is Element of bool the carrier' of C

ExX is set

{ b

( not b

ExX is Element of the carrier' of C

E1 is Element of the carrier of C

{ b

( not b

C is () ()

the carrier' of C is non empty set

bool the carrier' of C is non empty set

the carrier of C is non empty set

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

(C) is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

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

bool (bool the carrier' of C) is non empty set

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

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

X is Element of bool the carrier' of C

X is Element of bool the carrier' of C

(C) . X is Element of bool the carrier of C

(C) . X is Element of bool the carrier of C

ExX is set

{ b

( not b

ExX is Element of the carrier of C

E1 is Element of the carrier' of C

{ b

( not b

C is () ()

the carrier of C is non empty set

bool the carrier of C is non empty set

the carrier' of C is non empty set

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

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

bool (bool the carrier of C) is non empty set

(C) is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

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

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

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

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

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

X is Element of bool the carrier of C

(C) . X is Element of bool the carrier' of C

(C) . ((C) . X) is Element of bool the carrier of C

{ b

( not b

ExX is set

ExX is Element of the carrier' of C

ExX is set

ExX is Element of bool the carrier' of C

E1 is Element of the carrier of C

O is Element of the carrier' of C

InX is Element of the carrier' of C

(C) . ExX is Element of bool the carrier of C

{ b

( not b

C is () ()

the carrier' of C is non empty set

bool the carrier' of C is non empty set

the carrier of C is non empty set

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

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

bool (bool the carrier' of C) is non empty set

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

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

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

(C) is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

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

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

X is Element of bool the carrier' of C

(C) . X is Element of bool the carrier of C

(C) . ((C) . X) is Element of bool the carrier' of C

{ b

( not b

ExX is set

ExX is Element of the carrier of C

ExX is set

ExX is Element of bool the carrier of C

E1 is Element of the carrier' of C

O is Element of the carrier of C

InX is Element of the carrier of C

(C) . ExX is Element of bool the carrier' of C

{ b

( not b

C is () ()

the carrier of C is non empty set

bool the carrier of C is non empty set

the carrier' of C is non empty set

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

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

bool (bool the carrier of C) is non empty set

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

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

(C) is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

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

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

X is Element of bool the carrier of C

(C) . X is Element of bool the carrier' of C

(C) . ((C) . X) is Element of bool the carrier of C

(C) . ((C) . ((C) . X)) is Element of bool the carrier' of C

{ b

( not b

{ b

( not b

( not b

{ b

( not b

( not b

( not b

E1 is set

InX is Element of the carrier' of C

O is Element of the carrier' of C

InX is Element of the carrier of C

In is Element of the carrier' of C

In is Element of the carrier' of C

A9 is Element of the carrier' of C

E1 is set

InX is Element of the carrier' of C

O is Element of the carrier' of C

InX is Element of the carrier of C

In is Element of the carrier of C

E1 is set

O is Element of the carrier' of C

O is set

E1 is Element of bool the carrier' of C

InX is Element of the carrier of C

E1 is Element of bool the carrier' of C

O is Element of bool the carrier of C

(C) . E1 is Element of bool the carrier of C

C is () ()

the carrier' of C is non empty set

bool the carrier' of C is non empty set

the carrier of C is non empty set

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

(C) is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

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

bool (bool the carrier' of C) is non empty set

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

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

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

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

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

X is Element of bool the carrier' of C

(C) . X is Element of bool the carrier of C

(C) . ((C) . X) is Element of bool the carrier' of C

(C) . ((C) . ((C) . X)) is Element of bool the carrier of C

{ b

( not b

{ b

( not b

( not b

{ b

( not b

( not b

( not b

E1 is set

InX is Element of the carrier of C

O is Element of the carrier of C

InX is Element of the carrier' of C

In is Element of the carrier of C

In is Element of the carrier of C

A9 is Element of the carrier of C

E1 is set

InX is Element of the carrier of C

O is Element of the carrier of C

InX is Element of the carrier' of C

In is Element of the carrier' of C

E1 is set

O is Element of the carrier of C

O is set

E1 is Element of bool the carrier of C

InX is Element of the carrier' of C

E1 is Element of bool the carrier of C

O is Element of bool the carrier' of C

(C) . E1 is Element of bool the carrier' of C

C is () ()

the carrier of C is non empty set

bool the carrier of C is non empty set

the carrier' of C is non empty set

bool the carrier' of C is non empty set

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

bool (bool the carrier of C) is non empty set

(C) is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

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

bool (bool the carrier' of C) is non empty set

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

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

the of C is Relation-like the carrier of C -defined the carrier' of C -valued Element of bool [: the carrier of C, the carrier' of C:]

[: the carrier of C, the carrier' of C:] is non empty set

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

X is Element of bool the carrier of C

X is Element of bool the carrier' of C

(C) . X is Element of bool the carrier of C

[:X,X:] is Relation-like the carrier of C -defined the carrier' of C -valued Element of bool [: the carrier of C, the carrier' of C:]

ExX is set

ExX is Element of the carrier of C

E1 is Element of the carrier' of C

[ExX,E1] is V15() set

{ExX,E1} is non empty set

{ExX} is non empty set

{{ExX,E1},{ExX}} is non empty set

O is set

{ b

( not b

{ b

( not b

ExX is set

ExX is set

E1 is set

[ExX,E1] is V15() set

{ExX,E1} is non empty set

{ExX} is non empty set

{{ExX,E1},{ExX}} is non empty set

InX is Element of the carrier of C

O is Element of the carrier' of C

In is Element of the carrier of C

C is () ()

the carrier of C is non empty set

bool the carrier of C is non empty set

the carrier' of C is non empty set

bool the carrier' of C is non empty set

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

bool (bool the carrier' of C) is non empty set

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

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

bool (bool the carrier of C) is non empty set

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

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

the of C is Relation-like the carrier of C -defined the carrier' of C -valued Element of bool [: the carrier of C, the carrier' of C:]

[: the carrier of C, the carrier' of C:] is non empty set

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

X is Element of bool the carrier of C

(C) . X is Element of bool the carrier' of C

X is Element of bool the carrier' of C

[:X,X:] is Relation-like the carrier of C -defined the carrier' of C -valued Element of bool [: the carrier of C, the carrier' of C:]

ExX is set

ExX is Element of the carrier' of C

E1 is Element of the carrier of C

[E1,ExX] is V15() set

{E1,ExX} is non empty set

{E1} is non empty set

{{E1,ExX},{E1}} is non empty set

O is set

{ b

( not b

{ b

( not b

ExX is set

ExX is set

E1 is set

[ExX,E1] is V15() set

{ExX,E1} is non empty set

{ExX} is non empty set

{{ExX,E1},{ExX}} is non empty set

O is Element of the carrier' of C

InX is Element of the carrier of C

In is Element of the carrier' of C

C is () ()

the carrier of C is non empty set

bool the carrier of C is non empty set

the carrier' of C is non empty set

bool the carrier' of C is non empty set

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

bool (bool the carrier of C) is non empty set

(C) is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

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

bool (bool the carrier' of C) is non empty set

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

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

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

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

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

X is Element of bool the carrier of C

(C) . X is Element of bool the carrier' of C

X is Element of bool the carrier' of C

(C) . X is Element of bool the carrier of C

[:X,X:] is Relation-like the carrier of C -defined the carrier' of C -valued Element of bool [: the carrier of C, the carrier' of C:]

[: the carrier of C, the carrier' of C:] is non empty set

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

the of C is Relation-like the carrier of C -defined the carrier' of C -valued Element of bool [: the carrier of C, the carrier' of C:]

C is () ()

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

the carrier of C is non empty set

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

the carrier' of C is non empty set

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

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

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

BoolePoset the carrier of C is non empty strict V59() V60() V61() complete RelStr

the carrier of (BoolePoset the carrier of C) is non empty set

BoolePoset the carrier' of C is non empty strict V59() V60() V61() complete RelStr

the carrier of (BoolePoset the carrier' of C) is non empty set

[: the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier' of C):] is non empty set

bool [: the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier' of C):] is non empty set

rng (C) is Element of bool (bool the carrier' of C)

bool (bool the carrier' of C) is non empty set

X is set

BooleLatt the carrier' of C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V77() complemented Boolean complete LattStr

the carrier of (BooleLatt the carrier' of C) is non empty set

LattPOSet (BooleLatt the carrier' of C) is non empty strict V59() V60() V61() with_suprema with_infima complete V102() V103() RelStr

LattRel (BooleLatt the carrier' of C) is Relation-like the carrier of (BooleLatt the carrier' of C) -defined the carrier of (BooleLatt the carrier' of C) -valued V14( the carrier of (BooleLatt the carrier' of C)) V18( the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C)) V87() V90() V94() Element of bool [: the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C):]

[: the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C):] is non empty set

bool [: the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C):] is non empty set

RelStr(# the carrier of (BooleLatt the carrier' of C),(LattRel (BooleLatt the carrier' of C)) #) is strict RelStr

BooleLatt the carrier of C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V77() complemented Boolean complete LattStr

LattPOSet (BooleLatt the carrier of C) is non empty strict V59() V60() V61() with_suprema with_infima complete V102() V103() RelStr

the carrier of (BooleLatt the carrier of C) is non empty set

LattRel (BooleLatt the carrier of C) is Relation-like the carrier of (BooleLatt the carrier of C) -defined the carrier of (BooleLatt the carrier of C) -valued V14( the carrier of (BooleLatt the carrier of C)) V18( the carrier of (BooleLatt the carrier of C), the carrier of (BooleLatt the carrier of C)) V87() V90() V94() Element of bool [: the carrier of (BooleLatt the carrier of C), the carrier of (BooleLatt the carrier of C):]

[: the carrier of (BooleLatt the carrier of C), the carrier of (BooleLatt the carrier of C):] is non empty set

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

RelStr(# the carrier of (BooleLatt the carrier of C),(LattRel (BooleLatt the carrier of C)) #) is strict RelStr

dom (C) is Element of bool (bool the carrier of C)

bool (bool the carrier of C) is non empty set

X is set

the carrier of (LattPOSet (BooleLatt the carrier of C)) is non empty set

X is set

X is Relation-like the carrier of (BoolePoset the carrier of C) -defined the carrier of (BoolePoset the carrier' of C) -valued Function-like non empty V14( the carrier of (BoolePoset the carrier of C)) V18( the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier' of C)) Element of bool [: the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier' of C):]

C is () ()

(C) is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

the carrier' of C is non empty set

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

the carrier of C is non empty set

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

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

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

BoolePoset the carrier' of C is non empty strict V59() V60() V61() complete RelStr

the carrier of (BoolePoset the carrier' of C) is non empty set

BoolePoset the carrier of C is non empty strict V59() V60() V61() complete RelStr

the carrier of (BoolePoset the carrier of C) is non empty set

[: the carrier of (BoolePoset the carrier' of C), the carrier of (BoolePoset the carrier of C):] is non empty set

bool [: the carrier of (BoolePoset the carrier' of C), the carrier of (BoolePoset the carrier of C):] is non empty set

rng (C) is Element of bool (bool the carrier of C)

bool (bool the carrier of C) is non empty set

X is set

BooleLatt the carrier of C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V77() complemented Boolean complete LattStr

the carrier of (BooleLatt the carrier of C) is non empty set

LattPOSet (BooleLatt the carrier of C) is non empty strict V59() V60() V61() with_suprema with_infima complete V102() V103() RelStr

LattRel (BooleLatt the carrier of C) is Relation-like the carrier of (BooleLatt the carrier of C) -defined the carrier of (BooleLatt the carrier of C) -valued V14( the carrier of (BooleLatt the carrier of C)) V18( the carrier of (BooleLatt the carrier of C), the carrier of (BooleLatt the carrier of C)) V87() V90() V94() Element of bool [: the carrier of (BooleLatt the carrier of C), the carrier of (BooleLatt the carrier of C):]

[: the carrier of (BooleLatt the carrier of C), the carrier of (BooleLatt the carrier of C):] is non empty set

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

RelStr(# the carrier of (BooleLatt the carrier of C),(LattRel (BooleLatt the carrier of C)) #) is strict RelStr

BooleLatt the carrier' of C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V77() complemented Boolean complete LattStr

LattPOSet (BooleLatt the carrier' of C) is non empty strict V59() V60() V61() with_suprema with_infima complete V102() V103() RelStr

the carrier of (BooleLatt the carrier' of C) is non empty set

LattRel (BooleLatt the carrier' of C) is Relation-like the carrier of (BooleLatt the carrier' of C) -defined the carrier of (BooleLatt the carrier' of C) -valued V14( the carrier of (BooleLatt the carrier' of C)) V18( the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C)) V87() V90() V94() Element of bool [: the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C):]

[: the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C):] is non empty set

bool [: the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C):] is non empty set

RelStr(# the carrier of (BooleLatt the carrier' of C),(LattRel (BooleLatt the carrier' of C)) #) is strict RelStr

dom (C) is Element of bool (bool the carrier' of C)

bool (bool the carrier' of C) is non empty set

X is set

the carrier of (LattPOSet (BooleLatt the carrier' of C)) is non empty set

X is set

C is non empty RelStr

X is non empty RelStr

C is non empty V59() V60() V61() RelStr

X is non empty V59() V60() V61() RelStr

the carrier of C is non empty set

the carrier of X is non empty set

[: the carrier of C, the carrier of X:] is non empty set

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

[: the carrier of X, the carrier of C:] is non empty set

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

X is Connection of C,X

ExX is Relation-like the carrier of C -defined the carrier of X -valued Function-like non empty V14( the carrier of C) V18( the carrier of C, the carrier of X) Element of bool [: the carrier of C, the carrier of X:]

ExX is Relation-like the carrier of X -defined the carrier of C -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, the carrier of C) Element of bool [: the carrier of X, the carrier of C:]

[ExX,ExX] is V15() Connection of C,X

{ExX,ExX} is non empty set

{ExX} is non empty set

{{ExX,ExX},{ExX}} is non empty set

E1 is Element of the carrier of C

O is Element of the carrier of C

ExX . E1 is Element of the carrier of X

ExX . O is Element of the carrier of X

InX is Element of the carrier of X

In is Element of the carrier of X

ExX . (ExX . O) is Element of the carrier of C

E1 is Element of the carrier of X

O is Element of the carrier of X

ExX . E1 is Element of the carrier of C

ExX . O is Element of the carrier of C

InX is Element of the carrier of C

In is Element of the carrier of C

ExX . (ExX . O) is Element of the carrier of X

E1 is Element of the carrier of C

ExX . E1 is Element of the carrier of X

ExX . (ExX . E1) is Element of the carrier of C

O is Element of the carrier of X

ExX . O is Element of the carrier of C

ExX . (ExX . O) is Element of the carrier of X

E1 is Relation-like the carrier of C -defined the carrier of X -valued Function-like non empty V14( the carrier of C) V18( the carrier of C, the carrier of X) Element of bool [: the carrier of C, the carrier of X:]

O is Relation-like the carrier of X -defined the carrier of C -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, the carrier of C) Element of bool [: the carrier of X, the carrier of C:]

[E1,O] is V15() Connection of C,X

{E1,O} is non empty set

{E1} is non empty set

{{E1,O},{E1}} is non empty set

[ExX,ExX] `2 is set

X `2 is set

[E1,O] `2 is set

[ExX,ExX] `1 is set

X `1 is set

[E1,O] `1 is set

InX is Element of the carrier of C

ExX . InX is Element of the carrier of X

In is Element of the carrier of X

ExX . In is Element of the carrier of C

ExX . (ExX . InX) is Element of the carrier of C

InX is Element of the carrier of C

ExX . InX is Element of the carrier of X

In is Element of the carrier of X

ExX . In is Element of the carrier of C

ExX . (ExX . In) is Element of the carrier of X

InX is Element of the carrier of C

In is Element of the carrier of X

ExX . In is Element of the carrier of C

ExX . InX is Element of the carrier of X

A is Element of the carrier of X

A9 is Element of the carrier of C

ExX . A9 is Element of the carrier of X

ExX . A is Element of the carrier of C

E1 is Element of the carrier of C

O is Element of the carrier of X

ExX . O is Element of the carrier of C

ExX . E1 is Element of the carrier of X

In is Element of the carrier of X

InX is Element of the carrier of C

ExX . InX is Element of the carrier of X

ExX . In is Element of the carrier of C

A9 is Element of the carrier of C

A is Element of the carrier of X

ExX . A is Element of the carrier of C

ExX . A9 is Element of the carrier of X

p is Element of the carrier of X

p is Element of the carrier of C

ExX . p is Element of the carrier of X

ExX . p is Element of the carrier of C

C is non empty V59() V60() V61() RelStr

X is non empty V59() V60() V61() RelStr

the carrier of C is non empty set

the carrier of X is non empty set

[: the carrier of C, the carrier of X:] is non empty set

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

[: the carrier of X, the carrier of C:] is non empty set

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

X is Connection of C,X

ExX is Relation-like the carrier of C -defined the carrier of X -valued Function-like non empty V14( the carrier of C) V18( the carrier of C, the carrier of X) Element of bool [: the carrier of C, the carrier of X:]

ExX is Relation-like the carrier of X -defined the carrier of C -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, the carrier of C) Element of bool [: the carrier of X, the carrier of C:]

[ExX,ExX] is V15() Connection of C,X

{ExX,ExX} is non empty set

{ExX} is non empty set

{{ExX,ExX},{ExX}} is non empty set

E1 is Relation-like the carrier of C -defined the carrier of X -valued Function-like non empty V14( the carrier of C) V18( the carrier of C, the carrier of X) Element of bool [: the carrier of C, the carrier of X:]

O is Relation-like the carrier of X -defined the carrier of C -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, the carrier of C) Element of bool [: the carrier of X, the carrier of C:]

[E1,O] is V15() Connection of C,X

{E1,O} is non empty set

{E1} is non empty set

{{E1,O},{E1}} is non empty set

O * E1 is Relation-like the carrier of C -defined the carrier of C -valued Function-like non empty V14( the carrier of C) V18( the carrier of C, the carrier of C) Element of bool [: the carrier of C, the carrier of C:]

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

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

E1 * (O * E1) is Relation-like the carrier of C -defined the carrier of X -valued Function-like non empty V14( the carrier of C) V18( the carrier of C, the carrier of X) Element of bool [: the carrier of C, the carrier of X:]

E1 * O is Relation-like the carrier of X -defined the carrier of X -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, the carrier of X) Element of bool [: the carrier of X, the carrier of X:]

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

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

O * (E1 * O) is Relation-like the carrier of X -defined the carrier of C -valued Function-like non empty V14( the carrier of X) V18( the carrier of X, the carrier of C) Element of bool [: the carrier of X, the carrier of C:]

[E1,O] `1 is set

X `1 is set

[ExX,ExX] `1 is set

[E1,O] `2 is set

X `2 is set

[ExX,ExX] `2 is set

dom O is Element of bool the carrier of X

bool the carrier of X is non empty set

dom E1 is Element of bool the carrier of C

bool the carrier of C is non empty set

InX is set

E1 . InX is set

(E1 * (O * E1)) . InX is set

In is Element of the carrier of C

E1 . In is Element of the carrier of X

O . (E1 . In) is Element of the carrier of C

E1 . (O . (E1 . In)) is Element of the carrier of X

(O * E1) . In is Element of the carrier of C

E1 . ((O * E1) . In) is Element of the carrier of X

dom (O * E1) is Element of bool the carrier of C

InX is set

O . InX is set

(O * (E1 * O)) . InX is set

In is Element of the carrier of X

O . In is Element of the carrier of C

E1 . (O . In) is Element of the carrier of X

O . (E1 . (O . In)) is Element of the carrier of C

(E1 * O) . In is Element of the carrier of X

O . ((E1 * O) . In) is Element of the carrier of C

dom (E1 * O) is Element of bool the carrier of X

dom (E1 * (O * E1)) is Element of bool the carrier of C

dom (O * (E1 * O)) is Element of bool the carrier of X

C is () ()

the carrier of C is non empty set

BoolePoset the carrier of C is non empty strict V59() V60() V61() complete RelStr

the carrier' of C is non empty set

BoolePoset the carrier' of C is non empty strict V59() V60() V61() complete RelStr

(C) is Relation-like the carrier of (BoolePoset the carrier of C) -defined the carrier of (BoolePoset the carrier' of C) -valued Function-like non empty V14( the carrier of (BoolePoset the carrier of C)) V18( the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier' of C)) Element of bool [: the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier' of C):]

the carrier of (BoolePoset the carrier of C) is non empty set

the carrier of (BoolePoset the carrier' of C) is non empty set

[: the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier' of C):] is non empty set

bool [: the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier' of C):] is non empty set

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

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

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

(C) is Relation-like the carrier of (BoolePoset the carrier' of C) -defined the carrier of (BoolePoset the carrier of C) -valued Function-like non empty V14( the carrier of (BoolePoset the carrier' of C)) V18( the carrier of (BoolePoset the carrier' of C), the carrier of (BoolePoset the carrier of C)) Element of bool [: the carrier of (BoolePoset the carrier' of C), the carrier of (BoolePoset the carrier of C):]

[: the carrier of (BoolePoset the carrier' of C), the carrier of (BoolePoset the carrier of C):] is non empty set

bool [: the carrier of (BoolePoset the carrier' of C), the carrier of (BoolePoset the carrier of C):] is non empty set

(C) is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

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

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

[(C),(C)] is V15() Connection of BoolePoset the carrier of C, BoolePoset the carrier' of C

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

{(C)} is non empty set

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

BooleLatt the carrier' of C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V77() complemented Boolean complete LattStr

LattPOSet (BooleLatt the carrier' of C) is non empty strict V59() V60() V61() with_suprema with_infima complete V102() V103() RelStr

the carrier of (BooleLatt the carrier' of C) is non empty set

LattRel (BooleLatt the carrier' of C) is Relation-like the carrier of (BooleLatt the carrier' of C) -defined the carrier of (BooleLatt the carrier' of C) -valued V14( the carrier of (BooleLatt the carrier' of C)) V18( the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C)) V87() V90() V94() Element of bool [: the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C):]

[: the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C):] is non empty set

bool [: the carrier of (BooleLatt the carrier' of C), the carrier of (BooleLatt the carrier' of C):] is non empty set

RelStr(# the carrier of (BooleLatt the carrier' of C),(LattRel (BooleLatt the carrier' of C)) #) is strict RelStr

BooleLatt the carrier of C is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V77() complemented Boolean complete LattStr

LattPOSet (BooleLatt the carrier of C) is non empty strict V59() V60() V61() with_suprema with_infima complete V102() V103() RelStr

the carrier of (BooleLatt the carrier of C) is non empty set

LattRel (BooleLatt the carrier of C) is Relation-like the carrier of (BooleLatt the carrier of C) -defined the carrier of (BooleLatt the carrier of C) -valued V14( the carrier of (BooleLatt the carrier of C)) V18( the carrier of (BooleLatt the carrier of C), the carrier of (BooleLatt the carrier of C)) V87() V90() V94() Element of bool [: the carrier of (BooleLatt the carrier of C), the carrier of (BooleLatt the carrier of C):]

[: the carrier of (BooleLatt the carrier of C), the carrier of (BooleLatt the carrier of C):] is non empty set

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

RelStr(# the carrier of (BooleLatt the carrier of C),(LattRel (BooleLatt the carrier of C)) #) is strict RelStr

X is Element of the carrier of (BoolePoset the carrier of C)

(C) . X is Element of the carrier of (BoolePoset the carrier' of C)

X is Element of the carrier of (BoolePoset the carrier' of C)

(C) . X is Element of the carrier of (BoolePoset the carrier of C)

[X,((C) . X)] is V15() set

{X,((C) . X)} is non empty set

{X} is non empty set

{{X,((C) . X)},{X}} is non empty set

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

[: the carrier of (BoolePoset the carrier' of C), the carrier of (BoolePoset the carrier' of C):] is non empty set

bool [: the carrier of (BoolePoset the carrier' of C), the carrier of (BoolePoset the carrier' of C):] is non empty set

ExX is Element of the carrier of (BooleLatt the carrier of C)

O is Element of the carrier of (BooleLatt the carrier' of C)

ExX is Element of the carrier of (BooleLatt the carrier' of C)

O "\/" ExX is Element of the carrier of (BooleLatt the carrier' of C)

O \/ ExX is set

In is Element of bool the carrier' of C

InX is Element of bool the carrier' of C

A9 is set

(C) . InX is Element of bool the carrier of C

(C) . In is Element of bool the carrier of C

A9 is Element of the carrier of (BoolePoset the carrier' of C)

(C) . A9 is Element of the carrier of (BoolePoset the carrier of C)

A is Element of the carrier of (BooleLatt the carrier of C)

p is Element of bool the carrier of C

E1 is Element of bool the carrier of C

(C) . E1 is Element of bool the carrier' of C

(C) . ((C) . E1) is Element of bool the carrier of C

q is Element of bool the carrier of C

x is Element of the carrier of (BooleLatt the carrier of C)

p is Element of the carrier of (BooleLatt the carrier of C)

x "\/" p is Element of the carrier of (BooleLatt the carrier of C)

x \/ p is set

[x,((C) . A9)] is V15() set

{x,((C) . A9)} is non empty set

{x} is non empty set

{{x,((C) . A9)},{x}} is non empty set

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

[: the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier of C):] is non empty set

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

X is Element of the carrier of (BoolePoset the carrier of C)

(C) . X is Element of the carrier of (BoolePoset the carrier' of C)

X is Element of the carrier of (BoolePoset the carrier' of C)

(C) . X is Element of the carrier of (BoolePoset the carrier of C)

[X,((C) . X)] is V15() set

{X,((C) . X)} is non empty set

{X} is non empty set

{{X,((C) . X)},{X}} is non empty set

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

[: the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier of C):] is non empty set

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

ExX is Element of the carrier of (BooleLatt the carrier' of C)

O is Element of the carrier of (BooleLatt the carrier of C)

ExX is Element of the carrier of (BooleLatt the carrier of C)

O "\/" ExX is Element of the carrier of (BooleLatt the carrier of C)

O \/ ExX is set

In is Element of bool the carrier of C

InX is Element of bool the carrier of C

A9 is set

A is Element of bool the carrier of C

(C) . A is Element of bool the carrier' of C

A9 is Element of bool the carrier of C

(C) . A9 is Element of bool the carrier' of C

p is Element of the carrier of (BoolePoset the carrier of C)

(C) . p is Element of the carrier of (BoolePoset the carrier' of C)

p is Element of the carrier of (BooleLatt the carrier' of C)

q is Element of bool the carrier' of C

E1 is Element of bool the carrier' of C

(C) . E1 is Element of bool the carrier of C

(C) . ((C) . E1) is Element of bool the carrier' of C

x9 is Element of the carrier of (BooleLatt the carrier' of C)

x is Element of the carrier of (BooleLatt the carrier' of C)

x9 "\/" x is Element of the carrier of (BooleLatt the carrier' of C)

x9 \/ x is set

[x9,((C) . p)] is V15() set

{x9,((C) . p)} is non empty set

{x9} is non empty set

{{x9,((C) . p)},{x9}} is non empty set

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

[: the carrier of (BoolePoset the carrier' of C), the carrier of (BoolePoset the carrier' of C):] is non empty set

bool [: the carrier of (BoolePoset the carrier' of C), the carrier of (BoolePoset the carrier' of C):] is non empty set

C is () ()

the carrier of C is non empty set

bool the carrier of C is non empty set

the carrier' of C is non empty set

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

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

bool (bool the carrier of C) is non empty set

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

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

X is Element of bool the carrier of C

X is Element of bool the carrier of C

X \/ X is Element of bool the carrier of C

(C) . (X \/ X) is Element of bool the carrier' of C

(C) . X is Element of bool the carrier' of C

(C) . X is Element of bool the carrier' of C

((C) . X) /\ ((C) . X) is Element of bool the carrier' of C

ExX is Element of bool the carrier of C

(C) . ExX is Element of bool the carrier' of C

ExX is set

{ b

( not b

{ b

( not b

O is Element of the carrier' of C

E1 is Element of the carrier' of C

O is Element of the carrier of C

InX is Element of the carrier' of C

InX is Element of the carrier' of C

{ b

( not b

ExX is set

{ b

( not b

O is Element of the carrier' of C

E1 is Element of the carrier' of C

O is Element of the carrier of C

InX is Element of the carrier' of C

{ b

( not b

O is Element of the carrier of C

InX is Element of the carrier' of C

{ b

( not b

C is () ()

the carrier' of C is non empty set

bool the carrier' of C is non empty set

the carrier of C is non empty set

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

(C) is Relation-like bool the carrier' of C -defined bool the carrier of C -valued Function-like non empty V14( bool the carrier' of C) V18( bool the carrier' of C, bool the carrier of C) Element of bool [:(bool the carrier' of C),(bool the carrier of C):]

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

bool (bool the carrier' of C) is non empty set

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

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

X is Element of bool the carrier' of C

X is Element of bool the carrier' of C

X \/ X is Element of bool the carrier' of C

(C) . (X \/ X) is Element of bool the carrier of C

(C) . X is Element of bool the carrier of C

(C) . X is Element of bool the carrier of C

((C) . X) /\ ((C) . X) is Element of bool the carrier of C

ExX is Element of bool the carrier' of C

(C) . ExX is Element of bool the carrier of C

ExX is set

{ b

( not b

{ b

( not b

O is Element of the carrier of C

E1 is Element of the carrier of C

O is Element of the carrier' of C

InX is Element of the carrier of C

InX is Element of the carrier of C

{ b

( not b

ExX is set

{ b

( not b

O is Element of the carrier of C

E1 is Element of the carrier of C

O is Element of the carrier' of C

InX is Element of the carrier of C

{ b

( not b

O is Element of the carrier' of C

InX is Element of the carrier of C

{ b

( not b

C is () ()

(C) is Relation-like bool the carrier of C -defined bool the carrier' of C -valued Function-like non empty V14( bool the carrier of C) V18( bool the carrier of C, bool the carrier' of C) Element of bool [:(bool the carrier of C),(bool the carrier' of C):]

the carrier of C is non empty set

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

bool the carrier of C is non empty set

bool (bool the carrier of C) is non empty set

the carrier' of C is non empty set

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

bool the carrier' of C is non empty set

bool (bool the carrier' of C) is non empty set

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

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

(C) . {} is set

X is Element of bool the carrier of C

{ b

( not b

ExX is set

ExX is Element of the carrier' of C

ExX is set

ExX is Element of the carrier' of C

E1 is Element of the carrier of C

(C) . X is