:: CONLAT_1 semantic presentation

K118() is set
bool K118() is non 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 () ()
is non empty set
is non empty set
bool is non empty set

(,, 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
{ [b1, { b2 where b2 is Element of the carrier' of C : for b3 being Element of the carrier of C holds
( not b3 in b1 or not (C,b3,b2) )
}
]
where b1 is Element of bool the carrier of C : verum
}
is set

X is set
ExX is Element of bool the carrier of C
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in ExX or not (C,b2,b1) )
}
is set

[ExX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in ExX or not (C,b2,b1) )
}
]
is V15() set

{ExX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in ExX or not (C,b2,b1) )
}
}
is non empty set

{ExX} is non empty set
{{ExX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in ExX or not (C,b2,b1) )
}
}
,{ExX}
}
is non empty 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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
is set

[O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
]
is V15() set

{O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
}
is non empty set

{O} is non empty set
{{O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
}
,{O}
}
is non empty set

[ExX,ExX] `2 is set
[O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
]
`2 is set

InX is Element of bool the carrier of C
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
is set

[InX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
]
is V15() set

{InX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
}
is non empty set

{InX} is non empty set
{{InX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
}
,{InX}
}
is non empty set

[ExX,E1] `2 is set
[InX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
]
`2 is set

[O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
]
`1 is set

[ExX,ExX] `1 is set
[ExX,E1] `1 is set
[InX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
]
`1 is 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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
is set

[O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
]
is V15() set

{O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
}
is non empty set

{O} is non empty set
{{O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
}
,{O}
}
is non empty set

[ExX,E1] `1 is set
[O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
]
`1 is set

ExX is set
E1 is Element of bool the carrier of C
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in E1 or not (C,b2,b1) )
}
is set

[E1, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in E1 or not (C,b2,b1) )
}
]
is V15() set

{E1, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in E1 or not (C,b2,b1) )
}
}
is non empty set

{E1} is non empty set
{{E1, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in E1 or not (C,b2,b1) )
}
}
,{E1}
}
is non empty set

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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
is set

[O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
]
is V15() set

{O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
}
is non empty set

{O} is non empty set
{{O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
}
,{O}
}
is non empty set

InX is set
In is Element of the carrier' of C
[E1,ExX] `2 is set
[O, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in O or not (C,b2,b1) )
}
]
`2 is set

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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in E1 or not (C,b2,b1) )
}
is set

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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
is set

[InX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
]
is V15() set

{InX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
}
is non empty set

{InX} is non empty set
{{InX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
}
,{InX}
}
is non empty set

[E1,O] `2 is set
[InX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
]
`2 is set

[E1,O] `1 is set
[InX, { b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in InX or not (C,b2,b1) )
}
]
`1 is set

E1 is Element of bool the carrier of C
ExX . E1 is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in E1 or not (C,b2,b1) )
}
is set

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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in ExX or not (C,b2,b1) )
}
is set

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
{ [b1, { b2 where b2 is Element of the carrier of C : for b3 being Element of the carrier' of C holds
( not b3 in b1 or not (C,b2,b3) )
}
]
where b1 is Element of bool the carrier' of C : verum
}
is set

X is set
ExX is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in ExX or not (C,b1,b2) )
}
is set

[ExX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in ExX or not (C,b1,b2) )
}
]
is V15() set

{ExX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in ExX or not (C,b1,b2) )
}
}
is non empty set

{ExX} is non empty set
{{ExX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in ExX or not (C,b1,b2) )
}
}
,{ExX}
}
is non empty 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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
is set

[O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
]
is V15() set

{O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
}
is non empty set

{O} is non empty set
{{O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
}
,{O}
}
is non empty set

[ExX,ExX] `2 is set
[O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
]
`2 is set

InX is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
is set

[InX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
]
is V15() set

{InX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
}
is non empty set

{InX} is non empty set
{{InX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
}
,{InX}
}
is non empty set

[ExX,E1] `2 is set
[InX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
]
`2 is set

[O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
]
`1 is set

[ExX,ExX] `1 is set
[ExX,E1] `1 is set
[InX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
]
`1 is 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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
is set

[O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
]
is V15() set

{O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
}
is non empty set

{O} is non empty set
{{O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
}
,{O}
}
is non empty set

[ExX,E1] `1 is set
[O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
]
`1 is set

ExX is set
E1 is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in E1 or not (C,b1,b2) )
}
is set

[E1, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in E1 or not (C,b1,b2) )
}
]
is V15() set

{E1, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in E1 or not (C,b1,b2) )
}
}
is non empty set

{E1} is non empty set
{{E1, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in E1 or not (C,b1,b2) )
}
}
,{E1}
}
is non empty set

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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
is set

[O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
]
is V15() set

{O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
}
is non empty set

{O} is non empty set
{{O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
}
,{O}
}
is non empty set

InX is set
In is Element of the carrier of C
[E1,ExX] `2 is set
[O, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in O or not (C,b1,b2) )
}
]
`2 is set

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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in E1 or not (C,b1,b2) )
}
is set

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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
is set

[InX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
]
is V15() set

{InX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
}
is non empty set

{InX} is non empty set
{{InX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
}
,{InX}
}
is non empty set

[E1,O] `2 is set
[InX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
]
`2 is set

[E1,O] `1 is set
[InX, { b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in InX or not (C,b1,b2) )
}
]
`1 is set

E1 is Element of bool the carrier' of C
ExX . E1 is Element of bool the carrier of C
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in E1 or not (C,b1,b2) )
}
is set

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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in ExX or not (C,b1,b2) )
}
is set

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
{ b1 where b1 is Element of the carrier' of C : (C,X,b1) } is set
X is set
X is Element of bool the carrier of C
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is set

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
{ b1 where b1 is Element of the carrier of C : (C,b1,X) } is set
X is set
X is Element of bool the carrier' of C
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
is set

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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is set

ExX is Element of the carrier' of C
E1 is Element of the carrier of C
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is 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
(C) . X is Element of bool the carrier of C
(C) . X is Element of bool the carrier of C
ExX is set
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
is set

ExX is Element of the carrier of C
E1 is Element of the carrier' of C
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
is 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
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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is set

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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in ExX or not (C,b1,b2) )
}
is 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
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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
is set

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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in ExX or not (C,b2,b1) )
}
is 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
(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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is set

{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in { b1 where b3 is Element of the carrier' of C : for b4 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
or not (C,b1,b2) )
}
is set

{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in { b1 where b3 is Element of the carrier of C : for b4 being Element of the carrier' of C holds
( not b2 in { b1 where b5 is Element of the carrier' of C : for b6 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
or not (C,b1,b2) )
}
or not (C,b2,b1) )
}
is set

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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
is set

{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in { b1 where b3 is Element of the carrier of C : for b4 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
or not (C,b2,b1) )
}
is set

{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in { b1 where b3 is Element of the carrier' of C : for b4 being Element of the carrier of C holds
( not b2 in { b1 where b5 is Element of the carrier of C : for b6 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
or not (C,b2,b1) )
}
or not (C,b1,b2) )
}
is set

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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
is set

{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
is set

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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is set

{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is set

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

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

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

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

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

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

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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is set

{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is set

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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in ExX or not (C,b2,b1) )
}
is set

ExX is set
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in ExX or not (C,b2,b1) )
}
is set

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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is set

O is Element of the carrier of C
InX is Element of the carrier' of C
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is 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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
is set

{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
is set

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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in ExX or not (C,b1,b2) )
}
is set

ExX is set
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in ExX or not (C,b1,b2) )
}
is set

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
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
is set

O is Element of the carrier' of C
InX is Element of the carrier of C
{ b1 where b1 is Element of the carrier of C : for b2 being Element of the carrier' of C holds
( not b2 in X or not (C,b1,b2) )
}
is set

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
{ b1 where b1 is Element of the carrier' of C : for b2 being Element of the carrier of C holds
( not b2 in X or not (C,b2,b1) )
}
is set

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