:: 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₁, { b₂ where b₂ is Element of the carrier' of C : for b₃ being Element of the carrier of C holds
( not b₃ in b₁ or not (C,b₃,b₂) ) } ] where b₁ is Element of bool the carrier of C : verum } is set
X is set
ExX is Element of bool the carrier of C
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in ExX or not (C,b₂,b₁) ) } is set
[ExX, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in ExX or not (C,b₂,b₁) ) } ] is V15() set
{ExX, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in ExX or not (C,b₂,b₁) ) } } is non empty set
{ExX} is non empty set
{{ExX, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in ExX or not (C,b₂,b₁) ) } },{ExX}} is non empty set
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₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } is set
[O, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } ] is V15() set
{O, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } } is non empty set
{O} is non empty set
{{O, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } },{O}} is non empty set
[ExX,ExX] `2 is set
[O, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of C : for b<sub>2</sub> being Element of the carrier of C holds
( not b<sub>2</sub> in O or not (C,b<sub>2</sub>,b<sub>1</sub>) ) } ] `2 is set
InX is Element of bool the carrier of C
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in InX or not (C,b₂,b₁) ) } is set
[InX, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in InX or not (C,b₂,b₁) ) } ] is V15() set
{InX, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in InX or not (C,b₂,b₁) ) } } is non empty set
{InX} is non empty set
{{InX, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in InX or not (C,b₂,b₁) ) } },{InX}} is non empty set
[ExX,E1] `2 is set
[InX, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of C : for b<sub>2</sub> being Element of the carrier of C holds
( not b<sub>2</sub> in InX or not (C,b<sub>2</sub>,b<sub>1</sub>) ) } ] `2 is set
[O, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } ] `1 is set
[ExX,ExX] `1 is set
[ExX,E1] `1 is set
[InX, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of C : for b<sub>2</sub> being Element of the carrier of C holds
( not b<sub>2</sub> in InX or not (C,b<sub>2</sub>,b<sub>1</sub>) ) } ] `1 is set
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₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } is set
[O, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } ] is V15() set
{O, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } } is non empty set
{O} is non empty set
{{O, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } },{O}} is non empty set
[ExX,E1] `1 is set
[O, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of C : for b<sub>2</sub> being Element of the carrier of C holds
( not b<sub>2</sub> in O or not (C,b<sub>2</sub>,b<sub>1</sub>) ) } ] `1 is set
ExX is set
E1 is Element of bool the carrier of C
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in E1 or not (C,b₂,b₁) ) } is set
[E1, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in E1 or not (C,b₂,b₁) ) } ] is V15() set
{E1, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in E1 or not (C,b₂,b₁) ) } } is non empty set
{E1} is non empty set
{{E1, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in E1 or not (C,b₂,b₁) ) } },{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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } is set
[O, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } ] is V15() set
{O, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } } is non empty set
{O} is non empty set
{{O, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in O or not (C,b₂,b₁) ) } },{O}} is non empty set
InX is set
In is Element of the carrier' of C
[E1,ExX] `2 is set
[O, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of C : for b<sub>2</sub> being Element of the carrier of C holds
( not b<sub>2</sub> in O or not (C,b<sub>2</sub>,b<sub>1</sub>) ) } ] `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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in E1 or not (C,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in InX or not (C,b₂,b₁) ) } is set
[InX, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in InX or not (C,b₂,b₁) ) } ] is V15() set
{InX, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in InX or not (C,b₂,b₁) ) } } is non empty set
{InX} is non empty set
{{InX, { b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in InX or not (C,b₂,b₁) ) } },{InX}} is non empty set
[E1,O] `2 is set
[InX, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of C : for b<sub>2</sub> being Element of the carrier of C holds
( not b<sub>2</sub> in InX or not (C,b<sub>2</sub>,b<sub>1</sub>) ) } ] `2 is set
[E1,O] `1 is set
[InX, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of C : for b<sub>2</sub> being Element of the carrier of C holds
( not b<sub>2</sub> in InX or not (C,b<sub>2</sub>,b<sub>1</sub>) ) } ] `1 is set
E1 is Element of bool the carrier of C
ExX . E1 is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in E1 or not (C,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in ExX or not (C,b₂,b₁) ) } 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
{ [b₁, { b₂ where b₂ is Element of the carrier of C : for b₃ being Element of the carrier' of C holds
( not b₃ in b₁ or not (C,b₂,b₃) ) } ] where b₁ is Element of bool the carrier' of C : verum } is set
X is set
ExX is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in ExX or not (C,b₁,b₂) ) } is set
[ExX, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in ExX or not (C,b₁,b₂) ) } ] is V15() set
{ExX, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in ExX or not (C,b₁,b₂) ) } } is non empty set
{ExX} is non empty set
{{ExX, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in ExX or not (C,b₁,b₂) ) } },{ExX}} is non empty set
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₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } is set
[O, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } ] is V15() set
{O, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } } is non empty set
{O} is non empty set
{{O, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } },{O}} is non empty set
[ExX,ExX] `2 is set
[O, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of C : for b<sub>2</sub> being Element of the carrier' of C holds
( not b<sub>2</sub> in O or not (C,b<sub>1</sub>,b<sub>2</sub>) ) } ] `2 is set
InX is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in InX or not (C,b₁,b₂) ) } is set
[InX, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in InX or not (C,b₁,b₂) ) } ] is V15() set
{InX, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in InX or not (C,b₁,b₂) ) } } is non empty set
{InX} is non empty set
{{InX, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in InX or not (C,b₁,b₂) ) } },{InX}} is non empty set
[ExX,E1] `2 is set
[InX, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of C : for b<sub>2</sub> being Element of the carrier' of C holds
( not b<sub>2</sub> in InX or not (C,b<sub>1</sub>,b<sub>2</sub>) ) } ] `2 is set
[O, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } ] `1 is set
[ExX,ExX] `1 is set
[ExX,E1] `1 is set
[InX, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of C : for b<sub>2</sub> being Element of the carrier' of C holds
( not b<sub>2</sub> in InX or not (C,b<sub>1</sub>,b<sub>2</sub>) ) } ] `1 is set
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₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } is set
[O, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } ] is V15() set
{O, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } } is non empty set
{O} is non empty set
{{O, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } },{O}} is non empty set
[ExX,E1] `1 is set
[O, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of C : for b<sub>2</sub> being Element of the carrier' of C holds
( not b<sub>2</sub> in O or not (C,b<sub>1</sub>,b<sub>2</sub>) ) } ] `1 is set
ExX is set
E1 is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in E1 or not (C,b₁,b₂) ) } is set
[E1, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in E1 or not (C,b₁,b₂) ) } ] is V15() set
{E1, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in E1 or not (C,b₁,b₂) ) } } is non empty set
{E1} is non empty set
{{E1, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in E1 or not (C,b₁,b₂) ) } },{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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } is set
[O, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } ] is V15() set
{O, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } } is non empty set
{O} is non empty set
{{O, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in O or not (C,b₁,b₂) ) } },{O}} is non empty set
InX is set
In is Element of the carrier of C
[E1,ExX] `2 is set
[O, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of C : for b<sub>2</sub> being Element of the carrier' of C holds
( not b<sub>2</sub> in O or not (C,b<sub>1</sub>,b<sub>2</sub>) ) } ] `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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in E1 or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in InX or not (C,b₁,b₂) ) } is set
[InX, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in InX or not (C,b₁,b₂) ) } ] is V15() set
{InX, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in InX or not (C,b₁,b₂) ) } } is non empty set
{InX} is non empty set
{{InX, { b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in InX or not (C,b₁,b₂) ) } },{InX}} is non empty set
[E1,O] `2 is set
[InX, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of C : for b<sub>2</sub> being Element of the carrier' of C holds
( not b<sub>2</sub> in InX or not (C,b<sub>1</sub>,b<sub>2</sub>) ) } ] `2 is set
[E1,O] `1 is set
[InX, { b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of C : for b<sub>2</sub> being Element of the carrier' of C holds
( not b<sub>2</sub> in InX or not (C,b<sub>1</sub>,b<sub>2</sub>) ) } ] `1 is set
E1 is Element of bool the carrier' of C
ExX . E1 is Element of bool the carrier of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in E1 or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in ExX or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier' of C : (C,X,b₁) } is set
X is set
X is Element of bool the carrier of C
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of C : (C,b₁,X) } is set
X is set
X is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } is set
ExX is Element of the carrier' of C
E1 is Element of the carrier of C
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } is set
ExX is Element of the carrier of C
E1 is Element of the carrier' of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in ExX or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in ExX or not (C,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } is set
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in { b₁ where b₃ is Element of the carrier' of C : for b₄ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } or not (C,b₁,b₂) ) } is set
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in { b₁ where b₃ is Element of the carrier of C : for b₄ being Element of the carrier' of C holds
( not b₂ in { b₁ where b₅ is Element of the carrier' of C : for b₆ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } or not (C,b₁,b₂) ) } or not (C,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } is set
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in { b₁ where b₃ is Element of the carrier of C : for b₄ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } or not (C,b₂,b₁) ) } is set
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in { b₁ where b₃ is Element of the carrier' of C : for b₄ being Element of the carrier of C holds
( not b₂ in { b₁ where b₅ is Element of the carrier of C : for b₆ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } or not (C,b₂,b₁) ) } or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } is set
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } is set
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } 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
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₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } is set
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in ExX or not (C,b₂,b₁) ) } is set
ExX is set
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in ExX or not (C,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } is set
O is Element of the carrier of C
InX is Element of the carrier' of C
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } is set
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in ExX or not (C,b₁,b₂) ) } is set
ExX is set
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in ExX or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } is set
O is Element of the carrier' of C
InX is Element of the carrier of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in X or not (C,b₂,b₁) ) } 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 Element of bool 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
(C) . {} is set
X is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in X or not (C,b₁,b₂) ) } 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 Element of bool the carrier of C
C is 2-sorted
C is () 2-sorted
the carrier' of C is non empty set
bool the carrier' of C is non empty set
the non empty Element of bool the carrier' of C is non empty Element of bool the carrier' of C
the carrier of C is non empty set
bool the carrier of C is non empty set
the non empty Element of bool the carrier of C is non empty Element of bool the carrier of C
(C, the non empty Element of bool the carrier of C, the non empty Element of bool the carrier' of C) is (C) (C)
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
X is Element of bool the carrier of C
X is Element of bool the carrier' of C
(C,X,X) is (C) (C)
C is empty trivial V49() void V54( {} ) V55() trivial' 2-sorted
X is (C)
the of X is empty trivial non proper Element of bool the carrier of C
the carrier of C is empty trivial V34() set
bool the carrier of C is non empty set
the of X is empty trivial non proper Element of bool the carrier' of C
the carrier' of C is empty trivial set
bool the carrier' of C is non empty set
C is () 2-sorted
X is (C)
the of X is Element of bool the carrier of C
the carrier of C is set
bool the carrier of C is non empty set
the of X is Element of bool the carrier' of C
the carrier' of C is set
bool the carrier' of C is non empty set
the Element of the of X is Element of the of X
the Element of the of X is Element of the of X
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 (C)
the of X is Element of bool the carrier of C
(C) . the of X is Element of bool the carrier' of C
the of X is Element of bool the carrier' of C
C is () ()
C is () ()
the carrier of C is non empty set
the Element of the carrier of C is Element of the carrier of C
(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
{ the Element of the carrier of C} is non empty set
(C) . { the Element of the carrier of C} is set
ExX is set
ExX is set
ExX is Element of bool the carrier of C
{ b₁ where b₁ is Element of the carrier' of C : for b₂ being Element of the carrier of C holds
( not b₂ in ExX or not (C,b₂,b₁) ) } is set
E1 is Element of the carrier' of C
(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) . { the Element of the carrier of C}) is set
O is set
ExX is Element of bool the carrier of C
(C) . ExX is Element of bool the carrier' of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in (C) . ExX or not (C,b₁,b₂) ) } is set
InX is Element of the carrier of C
O is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,O,ExX) is (C) (C)
ExX is Element of bool the carrier of C
(C) . ExX is Element of bool the carrier' of C
(C) . ((C) . ExX) is Element of bool the carrier of C
In is (C) (C)
the of In is Element of bool the carrier of C
(C) . the of In is Element of bool the carrier' of C
the of In is Element of bool the carrier' of C
C is () ()
the (C) (C) (C) is (C) (C) (C)
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
the of the (C) (C) (C) is Element of bool the carrier of C
(C) . the of the (C) (C) (C) is Element of bool the carrier' of C
the of the (C) (C) (C) is Element of bool the carrier' of C
(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) . the of the (C) (C) (C) is Element of bool the carrier of C
(C, the of the (C) (C) (C), the of the (C) (C) (C)) is (C) (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
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
(C,((C) . ((C) . X)),((C) . X)) is (C) (C)
X is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,X,ExX) is (C) (C)
(C) . ExX is Element of bool the carrier of C
ExX is (C) (C) (C)
the of ExX is Element of bool the carrier of C
(C) . X is Element of bool the carrier' of C
the of ExX is Element of bool the carrier' of C
the of (C,((C) . ((C) . X)),((C) . X)) is Element of bool the carrier of C
(C) . the of (C,((C) . ((C) . X)),((C) . X)) is Element of bool the carrier' of C
the of (C,((C) . ((C) . X)),((C) . X)) is Element of bool the carrier' of C
X is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,X,ExX) is (C) (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
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
X is set
X is Element of bool the carrier' of C
(C,X,X) is (C) (C)
ExX is set
X is Element of bool the carrier' of C
(C,X,X) is (C) (C)
X is Element of bool the carrier' of C
(C,X,X) is (C) (C)
ExX is Element of bool the carrier' of C
(C,X,ExX) is (C) (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) . X),((C) . ((C) . X))) is (C) (C)
X is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,X,ExX) is (C) (C)
(C) . ExX is Element of bool the carrier of C
ExX is (C) (C) (C)
the of ExX is Element of bool the carrier of C
(C) . X is Element of bool the carrier' of C
the of ExX is Element of bool the carrier' of C
the of (C,((C) . X),((C) . ((C) . X))) is Element of bool the carrier' of C
(C) . the of (C,((C) . X),((C) . ((C) . X))) is Element of bool the carrier of C
the of (C,((C) . X),((C) . ((C) . X))) is Element of bool the carrier of C
X is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,X,ExX) is (C) (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
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
X is set
X is Element of bool the carrier of C
(C,X,X) is (C) (C)
ExX is set
X is Element of bool the carrier of C
(C,X,X) is (C) (C)
X is Element of bool the carrier of C
(C,X,X) is (C) (C)
ExX is Element of bool the carrier of C
(C,ExX,X) is (C) (C)
C is () ()
C is () ()
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
(C) . X is Element of bool the carrier of C
(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) . X) is Element of bool the carrier' of C
(C,((C) . X),((C) . ((C) . X))) is (C) (C)
(C) . {} is set
X is (C) (C) (C)
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
(C,((C) . ((C) . X)),((C) . X)) is (C) (C)
(C) . {} is set
X is (C) (C) (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
(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 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 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 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) . X),((C) . ((C) . X))) is (C) (C)
X is (C) (C) (C)
X is (C) (C) (C) (C) (C)
ExX is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,ExX,ExX) is (C) (C)
X is (C) (C) (C) (C) (C)
E1 is Element of bool the carrier of C
O is Element of bool the carrier' of C
(C,E1,O) is (C) (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
(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 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
(C) . {} is set
(C) . ((C) . {}) is 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)),((C) . X)) is (C) (C)
X is (C) (C) (C)
X is (C) (C) (C) (C) (C)
ExX is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,ExX,ExX) is (C) (C)
X is (C) (C) (C) (C) (C)
E1 is Element of bool the carrier of C
O is Element of bool the carrier' of C
(C,E1,O) is (C) (C)
C is () ()
(C) is (C) (C) (C) (C) (C)
the of (C) is Element of bool the carrier of C
the carrier of C is non empty set
bool the carrier of C is non empty set
(C) is (C) (C) (C) (C) (C)
the of (C) is Element of bool the carrier' of C
the carrier' of C is non empty set
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 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 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 set
(C) . {} is set
(C) . ((C) . {}) is set
X is Element of bool the carrier of C
X is Element of bool the carrier' of C
(C,X,X) is (C) (C)
ExX is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,ExX,ExX) is (C) (C)
C is () ()
X is (C) (C) (C)
the of X is Element of bool the carrier of C
the carrier of C is non empty set
bool the carrier of C is non empty set
the of X is Element of bool the carrier' of C
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) . the of X is Element of bool the carrier of C
(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) . the of X is Element of bool the carrier' of C
C is () ()
(C) is (C) (C) (C) (C) (C)
(C) is (C) (C) (C) (C) (C)
X is (C) (C) (C) (C)
the of X is Element of bool the carrier of C
the carrier of C is non empty set
bool the carrier of C is non empty set
the of X is Element of bool the carrier' of C
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) . the of X is Element of bool the carrier of C
(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) . the of X is Element of bool the carrier' of C
C is () ()
X is (C) (C)
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 (C) (C) (C)
the of X is Element of bool the carrier' of C
(C) . the of X is Element of bool the carrier of C
the of X is Element of bool the carrier of C
(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) . the of X is Element of bool the carrier' of C
C is () ()
(C) is (C) (C) (C) (C) (C)
(C) is (C) (C) (C) (C) (C)
X is (C) (C)
the of X is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
the of X is Element of bool the carrier of C
the carrier of C is non empty set
bool the carrier of C is non empty set
the of X is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
the of X is Element of bool the carrier of C
the carrier of C is non empty set
bool the carrier of C is non empty set
the of X is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
the of X is Element of bool the carrier of C
the carrier of C is non empty set
bool the carrier of C is non empty set
C is () ()
the (C) (C) (C) is (C) (C) (C)
{ the (C) (C) (C)} is non empty set
X is set
C is () ()
X is non empty (C)
X is Element of X
C is () ()
C is () ()
C is () ()
X is (C) (C) (C)
X is (C) (C) (C)
the of X is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
the of X is Element of 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
(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) . the of X is Element of bool the carrier of C
(C) . the of X is Element of bool the carrier of C
the of X is Element of bool the carrier of C
the of X is Element of bool the carrier of C
(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) . the of X is Element of bool the carrier' of C
(C) . the of X is Element of bool the carrier' of C
C is () ()
ExX is () ()
X is (C) (C) (C)
X is (C) (C) (C)
the of X is Element of bool the carrier' of C
the carrier' of C is non empty set
bool the carrier' of C is non empty set
the of X is Element of bool the carrier' of C
ExX is (ExX) (ExX) (ExX)
the of ExX is Element of bool the carrier' of ExX
the carrier' of ExX is non empty set
bool the carrier' of ExX is non empty set
E1 is (ExX) (ExX) (ExX)
the of E1 is Element of bool the carrier' of ExX
C is () ()
(C) is (C) (C) (C) (C) (C)
(C) is (C) (C) (C) (C) (C)
X is (C) (C) (C)
the carrier' of C is non empty set
the of (C) is Element of bool the carrier' of C
bool the carrier' of C is non empty set
the of X is Element of bool the carrier' of C
the carrier of C is non empty set
the of (C) is Element of bool the carrier of C
bool the carrier of C is non empty set
the of 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 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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
the (C) (C) (C) is (C) (C) (C)
the of the (C) (C) (C) is Element of bool the carrier of C
ExX is Element of bool the carrier of C
the of the (C) (C) (C) 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
(C) . ExX is Element of bool the carrier' of C
(C,ExX,ExX) is (C) (C)
X is non empty set
ExX is (C) (C) (C)
the of ExX is Element of bool the carrier of C
(C) . the of ExX is Element of bool the carrier' of C
the of ExX is Element of bool the carrier' of C
(C) . the of ExX is Element of bool the carrier of C
ExX is Element of bool the carrier of C
E1 is Element of bool the carrier' of C
(C,ExX,E1) is (C) (C)
(C) . ExX is Element of bool the carrier' of C
(C) . E1 is Element of bool the carrier of C
C is () ()
(C) is non empty set
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
X is set
X is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,X,ExX) is (C) (C)
(C) . X is Element of bool the carrier' of C
(C) . ExX is Element of bool the carrier of C
C is () ()
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
C is () ()
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
X is set
X is (C) (C) (C)
the of X is Element of bool the carrier' of C
the of X is Element of bool the carrier of C
(C) . the of X is Element of bool the carrier' of C
(C) . the of X is Element of bool the carrier of C
X is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,X,ExX) is (C) (C)
(C) . X is Element of bool the carrier' of C
(C) . ExX is Element of bool the carrier of C
C is () ()
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
X is (C) (C) (C,(C))
the of X is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
X is (C) (C) (C,(C))
the of X is Element of bool the carrier of C
the of X /\ the of X is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
the of X \/ the of X is Element of bool the carrier' of C
(C) . ( the of X \/ the of X) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ the of X)) is Element of bool the carrier' of C
(C,( the of X /\ the of X),((C) . ((C) . ( the of X \/ the of X)))) is (C) (C)
(C) . ((C) . ((C) . ( the of X \/ the of X))) 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) . the of X is Element of bool the carrier of C
(C) . the of X is Element of bool the carrier of C
((C) . the of X) /\ ((C) . the of X) is Element of bool the carrier of C
the of X /\ ((C) . the of X) is Element of bool the carrier of C
(C) . ( the of X /\ the of X) is Element of bool the carrier' of C
X is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
X is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
ExX is (C) (C) (C) (C)
ExX is (C) (C) (C) (C)
X . (ExX,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
X . [ExX,ExX] is set
the of ExX is Element of bool the carrier of C
the of ExX is Element of bool the carrier of C
the of ExX /\ the of ExX is Element of bool the carrier of C
the of ExX is Element of bool the carrier' of C
the of ExX is Element of bool the carrier' of C
the of ExX \/ the of ExX is Element of bool the carrier' of C
(C) . ( the of ExX \/ the of ExX) is Element of bool the carrier of C
(C) . ((C) . ( the of ExX \/ the of ExX)) is Element of bool the carrier' of C
ExX is (C) (C) (C) (C)
ExX is (C) (C) (C) (C)
X . (ExX,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
X . [ExX,ExX] is set
the of ExX is Element of bool the carrier of C
the of ExX is Element of bool the carrier of C
the of ExX /\ the of ExX is Element of bool the carrier of C
the of ExX is Element of bool the carrier' of C
the of ExX is Element of bool the carrier' of C
the of ExX \/ the of ExX is Element of bool the carrier' of C
(C) . ( the of ExX \/ the of ExX) is Element of bool the carrier of C
(C) . ((C) . ( the of ExX \/ the of ExX)) is Element of bool the carrier' of C
X is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
X is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
ExX is set
X . ExX is set
X . 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 (C) (C) (C) (C)
O is (C) (C) (C) (C)
X . (InX,O) is set
[InX,O] is V15() set
{InX,O} is non empty set
{InX} is non empty set
{{InX,O},{InX}} is non empty set
X . [InX,O] is set
the of InX is Element of bool the carrier of C
the of O is Element of bool the carrier of C
the of InX /\ the of O is Element of bool the carrier of C
the of InX is Element of bool the carrier' of C
the of O is Element of bool the carrier' of C
the of InX \/ the of O is Element of bool the carrier' of C
(C) . ( the of InX \/ the of O) is Element of bool the carrier of C
(C) . ((C) . ( the of InX \/ the of O)) is Element of bool the carrier' of C
X . (InX,O) is set
X . [InX,O] is set
In is Element of bool the carrier of C
A9 is Element of bool the carrier' of C
(C,In,A9) is (C) (C)
A is Element of bool the carrier of C
p is Element of bool the carrier' of C
(C,A,p) is (C) (C)
dom X is Relation-like (C) -defined (C) -valued Element of bool [:(C),(C):]
bool [:(C),(C):] is non empty set
dom X is Relation-like (C) -defined (C) -valued Element of bool [:(C),(C):]
C is () ()
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
X is (C) (C) (C,(C))
the of X is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
X is (C) (C) (C,(C))
the of X is Element of bool the carrier of C
the of X \/ the of X is Element of bool the carrier of C
(C) . ( the of X \/ the of X) is Element of bool the carrier' of C
(C) . ((C) . ( the of X \/ the of X)) is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
the of X /\ the of X is Element of bool the carrier' of C
(C,((C) . ((C) . ( the of X \/ the of X))),( the of X /\ the of X)) is (C) (C)
(C) . ((C) . ((C) . ( the of X \/ the of X))) 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) . the of X is Element of bool the carrier' of C
(C) . the of X is Element of bool the carrier' of C
((C) . the of X) /\ ((C) . the of X) is Element of bool the carrier' of C
the of X /\ ((C) . the of X) is Element of bool the carrier' of C
(C) . ( the of X /\ the of X) is Element of bool the carrier of C
X is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
X is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
ExX is (C) (C) (C) (C)
ExX is (C) (C) (C) (C)
X . (ExX,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
X . [ExX,ExX] is set
the of ExX is Element of bool the carrier of C
the of ExX is Element of bool the carrier of C
the of ExX \/ the of ExX is Element of bool the carrier of C
(C) . ( the of ExX \/ the of ExX) is Element of bool the carrier' of C
(C) . ((C) . ( the of ExX \/ the of ExX)) is Element of bool the carrier of C
the of ExX is Element of bool the carrier' of C
the of ExX is Element of bool the carrier' of C
the of ExX /\ the of ExX is Element of bool the carrier' of C
ExX is (C) (C) (C) (C)
ExX is (C) (C) (C) (C)
X . (ExX,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
X . [ExX,ExX] is set
the of ExX is Element of bool the carrier of C
the of ExX is Element of bool the carrier of C
the of ExX \/ the of ExX is Element of bool the carrier of C
(C) . ( the of ExX \/ the of ExX) is Element of bool the carrier' of C
(C) . ((C) . ( the of ExX \/ the of ExX)) is Element of bool the carrier of C
the of ExX is Element of bool the carrier' of C
the of ExX is Element of bool the carrier' of C
the of ExX /\ the of ExX is Element of bool the carrier' of C
X is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
X is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
ExX is set
X . ExX is set
X . 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 (C) (C) (C) (C)
O is (C) (C) (C) (C)
X . (InX,O) is set
[InX,O] is V15() set
{InX,O} is non empty set
{InX} is non empty set
{{InX,O},{InX}} is non empty set
X . [InX,O] is set
the of InX is Element of bool the carrier of C
the of O is Element of bool the carrier of C
the of InX \/ the of O is Element of bool the carrier of C
(C) . ( the of InX \/ the of O) is Element of bool the carrier' of C
(C) . ((C) . ( the of InX \/ the of O)) is Element of bool the carrier of C
the of InX is Element of bool the carrier' of C
the of O is Element of bool the carrier' of C
the of InX /\ the of O is Element of bool the carrier' of C
X . (InX,O) is set
X . [InX,O] is set
In is Element of bool the carrier of C
A9 is Element of bool the carrier' of C
(C,In,A9) is (C) (C)
A is Element of bool the carrier of C
p is Element of bool the carrier' of C
(C,A,p) is (C) (C)
dom X is Relation-like (C) -defined (C) -valued Element of bool [:(C),(C):]
bool [:(C),(C):] is non empty set
dom X is Relation-like (C) -defined (C) -valued Element of bool [:(C),(C):]
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
rng (C) is Element of bool (C)
bool (C) is non empty set
X is (C) (C) (C) (C)
X is (C) (C) (C) (C)
(C) . (X,X) is set
[X,X] is V15() set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
(C) . [X,X] is set
dom (C) is Relation-like (C) -defined (C) -valued Element of bool [:(C),(C):]
bool [:(C),(C):] is non empty set
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
rng (C) is Element of bool (C)
bool (C) is non empty set
X is (C) (C) (C) (C)
X is (C) (C) (C) (C)
(C) . (X,X) is set
[X,X] is V15() set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
(C) . [X,X] is set
dom (C) is Relation-like (C) -defined (C) -valued Element of bool [:(C),(C):]
bool [:(C),(C):] is non empty set
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
X is (C) (C) (C) (C)
X is (C) (C) (C) (C)
(C) . (X,X) is set
[X,X] is V15() set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
(C) . [X,X] is set
(C) . (X,X) is set
[X,X] is V15() set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
(C) . [X,X] is set
the of X is Element of bool the carrier of C
the of X is Element of bool the carrier of C
the of X /\ the of X is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
the of X is Element of bool the carrier' of C
the of X \/ the of X is Element of bool the carrier' of C
(C) . ( the of X \/ the of X) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ the of X)) is Element of bool the carrier' of C
the of X /\ the of X is Element of bool the carrier of C
the of X \/ the of X is Element of bool the carrier' of C
(C) . ( the of X \/ the of X) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ the of X)) is Element of bool the carrier' of C
ExX is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,ExX,ExX) is (C) (C)
E1 is Element of bool the carrier of C
O is Element of bool the carrier' of C
(C,E1,O) is (C) (C)
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
X is (C) (C) (C) (C)
X is (C) (C) (C) (C)
(C) . (X,X) is set
[X,X] is V15() set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
(C) . [X,X] is set
(C) . (X,X) is set
[X,X] is V15() set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
(C) . [X,X] is set
the of X is Element of bool the carrier of C
the of X is Element of bool the carrier of C
the of X \/ the of X is Element of bool the carrier of C
(C) . ( the of X \/ the of X) is Element of bool the carrier' of C
(C) . ((C) . ( the of X \/ the of X)) is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
the of X is Element of bool the carrier' of C
the of X /\ the of X is Element of bool the carrier' of C
the of X \/ the of X is Element of bool the carrier of C
(C) . ( the of X \/ the of X) is Element of bool the carrier' of C
(C) . ((C) . ( the of X \/ the of X)) is Element of bool the carrier of C
the of X /\ the of X is Element of bool the carrier' of C
ExX is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,ExX,ExX) is (C) (C)
E1 is Element of bool the carrier of C
O is Element of bool the carrier' of C
(C,E1,O) is (C) (C)
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
X is (C) (C) (C) (C)
X is (C) (C) (C) (C)
ExX is (C) (C) (C) (C)
(C) . (X,ExX) is set
[X,ExX] is V15() set
{X,ExX} is non empty set
{X} is non empty set
{{X,ExX},{X}} is non empty set
(C) . [X,ExX] is set
(C) . (X,((C) . (X,ExX))) is set
[X,((C) . (X,ExX))] is V15() set
{X,((C) . (X,ExX))} is non empty set
{X} is non empty set
{{X,((C) . (X,ExX))},{X}} is non empty set
(C) . [X,((C) . (X,ExX))] is set
(C) . (X,X) is set
[X,X] is V15() set
{X,X} is non empty set
{{X,X},{X}} is non empty set
(C) . [X,X] is set
(C) . (((C) . (X,X)),ExX) is set
[((C) . (X,X)),ExX] is V15() set
{((C) . (X,X)),ExX} is non empty set
{((C) . (X,X))} is non empty set
{{((C) . (X,X)),ExX},{((C) . (X,X))}} is non empty set
(C) . [((C) . (X,X)),ExX] is set
rng (C) is Element of bool (C)
bool (C) is non empty set
the of X is Element of bool the carrier of C
the of X is Element of bool the carrier of C
the of X /\ the of X is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
the of X is Element of bool the carrier' of C
the of X \/ the of X is Element of bool the carrier' of C
(C) . ( the of X \/ the of X) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ the of X)) is Element of bool the carrier' of C
ExX is (C) (C) (C) (C)
(C) . (ExX,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
(C) . [ExX,ExX] is set
the of ExX is Element of bool the carrier of C
the of ExX is Element of bool the carrier of C
the of ExX /\ the of ExX is Element of bool the carrier of C
the of ExX is Element of bool the carrier' of C
the of ExX is Element of bool the carrier' of C
the of ExX \/ the of ExX is Element of bool the carrier' of C
(C) . ( the of ExX \/ the of ExX) is Element of bool the carrier of C
(C) . ((C) . ( the of ExX \/ the of ExX)) is Element of bool the carrier' of C
the of X /\ the of ExX is Element of bool the carrier of C
the of X \/ the of ExX is Element of bool the carrier' of C
(C) . ( the of X \/ the of ExX) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ the of ExX)) is Element of bool the carrier' of C
E1 is (C) (C) (C) (C)
(C) . (X,E1) is set
[X,E1] is V15() set
{X,E1} is non empty set
{{X,E1},{X}} is non empty set
(C) . [X,E1] is set
the of E1 is Element of bool the carrier of C
the of X /\ the of E1 is Element of bool the carrier of C
the of E1 is Element of bool the carrier' of C
the of X \/ the of E1 is Element of bool the carrier' of C
(C) . ( the of X \/ the of E1) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ the of E1)) is Element of bool the carrier' of C
the of X \/ ((C) . ((C) . ( the of X \/ the of ExX))) is Element of bool the carrier' of C
(C) . ( the of X \/ ((C) . ((C) . ( the of X \/ the of ExX)))) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ ((C) . ((C) . ( the of X \/ the of ExX))))) is Element of bool the carrier' of C
(C) . the of X is Element of bool the carrier of C
(C) . ((C) . ((C) . ( the of X \/ the of ExX))) is Element of bool the carrier of C
((C) . the of X) /\ ((C) . ((C) . ((C) . ( the of X \/ the of ExX)))) is Element of bool the carrier of C
(C) . (((C) . the of X) /\ ((C) . ((C) . ((C) . ( the of X \/ the of ExX))))) is Element of bool the carrier' of C
((C) . the of X) /\ ((C) . ( the of X \/ the of ExX)) is Element of bool the carrier of C
(C) . (((C) . the of X) /\ ((C) . ( the of X \/ the of ExX))) is Element of bool the carrier' of C
(C) . the of X is Element of bool the carrier of C
(C) . the of ExX is Element of bool the carrier of C
((C) . the of X) /\ ((C) . the of ExX) is Element of bool the carrier of C
((C) . the of X) /\ (((C) . the of X) /\ ((C) . the of ExX)) is Element of bool the carrier of C
(C) . (((C) . the of X) /\ (((C) . the of X) /\ ((C) . the of ExX))) is Element of bool the carrier' of C
((C) . the of X) /\ ((C) . the of X) is Element of bool the carrier of C
(((C) . the of X) /\ ((C) . the of X)) /\ ((C) . the of ExX) is Element of bool the carrier of C
(C) . ((((C) . the of X) /\ ((C) . the of X)) /\ ((C) . the of ExX)) is Element of bool the carrier' of C
((C) . ( the of X \/ the of X)) /\ ((C) . the of ExX) is Element of bool the carrier of C
(C) . (((C) . ( the of X \/ the of X)) /\ ((C) . the of ExX)) is Element of bool the carrier' of C
(C) . ((C) . ((C) . ( the of X \/ the of X))) is Element of bool the carrier of C
((C) . ((C) . ((C) . ( the of X \/ the of X)))) /\ ((C) . the of ExX) is Element of bool the carrier of C
(C) . (((C) . ((C) . ((C) . ( the of X \/ the of X)))) /\ ((C) . the of ExX)) is Element of bool the carrier' of C
((C) . ((C) . ( the of X \/ the of X))) \/ the of ExX is Element of bool the carrier' of C
(C) . (((C) . ((C) . ( the of X \/ the of X))) \/ the of ExX) is Element of bool the carrier of C
(C) . ((C) . (((C) . ((C) . ( the of X \/ the of X))) \/ the of ExX)) is Element of bool the carrier' of C
O is Element of bool the carrier of C
InX is Element of bool the carrier' of C
(C,O,InX) is (C) (C)
In is Element of bool the carrier of C
A9 is Element of bool the carrier' of C
(C,In,A9) is (C) (C)
A is Element of bool the carrier of C
p is Element of bool the carrier' of C
(C,A,p) is (C) (C)
p is Element of bool the carrier of C
q is Element of bool the carrier' of C
(C,p,q) is (C) (C)
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
X is (C) (C) (C) (C)
X is (C) (C) (C) (C)
ExX is (C) (C) (C) (C)
(C) . (X,ExX) is set
[X,ExX] is V15() set
{X,ExX} is non empty set
{X} is non empty set
{{X,ExX},{X}} is non empty set
(C) . [X,ExX] is set
(C) . (X,((C) . (X,ExX))) is set
[X,((C) . (X,ExX))] is V15() set
{X,((C) . (X,ExX))} is non empty set
{X} is non empty set
{{X,((C) . (X,ExX))},{X}} is non empty set
(C) . [X,((C) . (X,ExX))] is set
(C) . (X,X) is set
[X,X] is V15() set
{X,X} is non empty set
{{X,X},{X}} is non empty set
(C) . [X,X] is set
(C) . (((C) . (X,X)),ExX) is set
[((C) . (X,X)),ExX] is V15() set
{((C) . (X,X)),ExX} is non empty set
{((C) . (X,X))} is non empty set
{{((C) . (X,X)),ExX},{((C) . (X,X))}} is non empty set
(C) . [((C) . (X,X)),ExX] is set
rng (C) is Element of bool (C)
bool (C) is non empty set
the of X is Element of bool the carrier of C
the of X is Element of bool the carrier of C
the of X \/ the of X is Element of bool the carrier of C
(C) . ( the of X \/ the of X) is Element of bool the carrier' of C
(C) . ((C) . ( the of X \/ the of X)) is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
the of X is Element of bool the carrier' of C
the of X /\ the of X is Element of bool the carrier' of C
ExX is (C) (C) (C) (C)
(C) . (ExX,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
(C) . [ExX,ExX] is set
the of ExX is Element of bool the carrier of C
the of ExX is Element of bool the carrier of C
the of ExX \/ the of ExX is Element of bool the carrier of C
(C) . ( the of ExX \/ the of ExX) is Element of bool the carrier' of C
(C) . ((C) . ( the of ExX \/ the of ExX)) is Element of bool the carrier of C
the of ExX is Element of bool the carrier' of C
the of ExX is Element of bool the carrier' of C
the of ExX /\ the of ExX is Element of bool the carrier' of C
the of X \/ the of ExX is Element of bool the carrier of C
(C) . ( the of X \/ the of ExX) is Element of bool the carrier' of C
(C) . ((C) . ( the of X \/ the of ExX)) is Element of bool the carrier of C
the of X /\ the of ExX is Element of bool the carrier' of C
E1 is (C) (C) (C) (C)
(C) . (X,E1) is set
[X,E1] is V15() set
{X,E1} is non empty set
{{X,E1},{X}} is non empty set
(C) . [X,E1] is set
the of E1 is Element of bool the carrier of C
the of X \/ the of E1 is Element of bool the carrier of C
(C) . ( the of X \/ the of E1) is Element of bool the carrier' of C
(C) . ((C) . ( the of X \/ the of E1)) is Element of bool the carrier of C
the of E1 is Element of bool the carrier' of C
the of X /\ the of E1 is Element of bool the carrier' of C
the of X \/ ((C) . ((C) . ( the of X \/ the of ExX))) is Element of bool the carrier of C
(C) . ( the of X \/ ((C) . ((C) . ( the of X \/ the of ExX)))) is Element of bool the carrier' of C
(C) . ((C) . ( the of X \/ ((C) . ((C) . ( the of X \/ the of ExX))))) is Element of bool the carrier of C
(C) . the of X is Element of bool the carrier' of C
(C) . ((C) . ((C) . ( the of X \/ the of ExX))) is Element of bool the carrier' of C
((C) . the of X) /\ ((C) . ((C) . ((C) . ( the of X \/ the of ExX)))) is Element of bool the carrier' of C
(C) . (((C) . the of X) /\ ((C) . ((C) . ((C) . ( the of X \/ the of ExX))))) is Element of bool the carrier of C
((C) . the of X) /\ ((C) . ( the of X \/ the of ExX)) is Element of bool the carrier' of C
(C) . (((C) . the of X) /\ ((C) . ( the of X \/ the of ExX))) is Element of bool the carrier of C
(C) . the of X is Element of bool the carrier' of C
(C) . the of ExX is Element of bool the carrier' of C
((C) . the of X) /\ ((C) . the of ExX) is Element of bool the carrier' of C
((C) . the of X) /\ (((C) . the of X) /\ ((C) . the of ExX)) is Element of bool the carrier' of C
(C) . (((C) . the of X) /\ (((C) . the of X) /\ ((C) . the of ExX))) is Element of bool the carrier of C
((C) . the of X) /\ ((C) . the of X) is Element of bool the carrier' of C
(((C) . the of X) /\ ((C) . the of X)) /\ ((C) . the of ExX) is Element of bool the carrier' of C
(C) . ((((C) . the of X) /\ ((C) . the of X)) /\ ((C) . the of ExX)) is Element of bool the carrier of C
((C) . ( the of X \/ the of X)) /\ ((C) . the of ExX) is Element of bool the carrier' of C
(C) . (((C) . ( the of X \/ the of X)) /\ ((C) . the of ExX)) is Element of bool the carrier of C
(C) . ((C) . ((C) . ( the of X \/ the of X))) is Element of bool the carrier' of C
((C) . ((C) . ((C) . ( the of X \/ the of X)))) /\ ((C) . the of ExX) is Element of bool the carrier' of C
(C) . (((C) . ((C) . ((C) . ( the of X \/ the of X)))) /\ ((C) . the of ExX)) is Element of bool the carrier of C
((C) . ((C) . ( the of X \/ the of X))) \/ the of ExX is Element of bool the carrier of C
(C) . (((C) . ((C) . ( the of X \/ the of X))) \/ the of ExX) is Element of bool the carrier' of C
(C) . ((C) . (((C) . ((C) . ( the of X \/ the of X))) \/ the of ExX)) is Element of bool the carrier of C
O is Element of bool the carrier of C
InX is Element of bool the carrier' of C
(C,O,InX) is (C) (C)
In is Element of bool the carrier of C
A9 is Element of bool the carrier' of C
(C,In,A9) is (C) (C)
A is Element of bool the carrier of C
p is Element of bool the carrier' of C
(C,A,p) is (C) (C)
p is Element of bool the carrier of C
q is Element of bool the carrier' of C
(C,p,q) is (C) (C)
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
X is (C) (C) (C) (C)
X is (C) (C) (C) (C)
(C) . (X,X) is set
[X,X] is V15() set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
(C) . [X,X] is set
(C) . (((C) . (X,X)),X) is set
[((C) . (X,X)),X] is V15() set
{((C) . (X,X)),X} is non empty set
{((C) . (X,X))} is non empty set
{{((C) . (X,X)),X},{((C) . (X,X))}} is non empty set
(C) . [((C) . (X,X)),X] is set
the of X is Element of bool the carrier of C
the of X is Element of bool the carrier of C
the of X /\ the of X is Element of bool the carrier of C
rng (C) is Element of bool (C)
bool (C) is non empty set
the of X is Element of bool the carrier' of C
the of X is Element of bool the carrier' of C
the of X \/ the of X is Element of bool the carrier' of C
(C) . ( the of X \/ the of X) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ the of X)) is Element of bool the carrier' of C
ExX is (C) (C) (C) (C)
(C) . (ExX,X) is set
[ExX,X] is V15() set
{ExX,X} is non empty set
{ExX} is non empty set
{{ExX,X},{ExX}} is non empty set
(C) . [ExX,X] is set
the of ExX is Element of bool the carrier of C
the of ExX \/ the of X is Element of bool the carrier of C
(C) . ( the of ExX \/ the of X) is Element of bool the carrier' of C
(C) . ((C) . ( the of ExX \/ the of X)) is Element of bool the carrier of C
the of ExX is Element of bool the carrier' of C
the of ExX /\ the of X is Element of bool the carrier' of C
( the of X /\ the of X) \/ the of X is Element of bool the carrier of C
(C) . (( the of X /\ the of X) \/ the of X) is Element of bool the carrier' of C
(C) . ((C) . (( the of X /\ the of X) \/ the of X)) is Element of bool the carrier of C
(C) . ( the of X /\ the of X) is Element of bool the carrier' of C
(C) . the of X is Element of bool the carrier' of C
((C) . ( the of X /\ the of X)) /\ ((C) . the of X) is Element of bool the carrier' of C
(C) . (((C) . ( the of X /\ the of X)) /\ ((C) . the of X)) is Element of bool the carrier of C
(C) . ((C) . the of X) is Element of bool the carrier of C
(C) . the of X is Element of bool the carrier of C
((C) . ((C) . ( the of X \/ the of X))) /\ the of X is Element of bool the carrier' of C
(C) . the of X is Element of bool the carrier of C
((C) . the of X) /\ ((C) . the of X) is Element of bool the carrier of C
(C) . (((C) . the of X) /\ ((C) . the of X)) is Element of bool the carrier' of C
((C) . (((C) . the of X) /\ ((C) . the of X))) /\ the of X is Element of bool the carrier' of C
the of X /\ ((C) . the of X) is Element of bool the carrier of C
(C) . ( the of X /\ ((C) . the of X)) is Element of bool the carrier' of C
((C) . ( the of X /\ ((C) . the of X))) /\ the of X is Element of bool the carrier' of C
((C) . ( the of X /\ the of X)) /\ the of X is Element of bool the carrier' of C
ExX is Element of bool the carrier of C
E1 is Element of bool the carrier' of C
(C,ExX,E1) is (C) (C)
O is Element of bool the carrier of C
InX is Element of bool the carrier' of C
(C,O,InX) is (C) (C)
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
X is (C) (C) (C) (C)
X is (C) (C) (C) (C)
(C) . (X,X) is set
[X,X] is V15() set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
(C) . [X,X] is set
(C) . (X,((C) . (X,X))) is set
[X,((C) . (X,X))] is V15() set
{X,((C) . (X,X))} is non empty set
{{X,((C) . (X,X))},{X}} is non empty set
(C) . [X,((C) . (X,X))] is set
the of X is Element of bool the carrier' of C
the of X is Element of bool the carrier' of C
the of X /\ the of X is Element of bool the carrier' of C
rng (C) is Element of bool (C)
bool (C) is non empty set
the of X is Element of bool the carrier of C
the of X is Element of bool the carrier of C
the of X \/ the of X is Element of bool the carrier of C
(C) . ( the of X \/ the of X) is Element of bool the carrier' of C
(C) . ((C) . ( the of X \/ the of X)) is Element of bool the carrier of C
ExX is (C) (C) (C) (C)
(C) . (X,ExX) is set
[X,ExX] is V15() set
{X,ExX} is non empty set
{{X,ExX},{X}} is non empty set
(C) . [X,ExX] is set
the of ExX is Element of bool the carrier of C
the of X /\ the of ExX is Element of bool the carrier of C
the of ExX is Element of bool the carrier' of C
the of X \/ the of ExX is Element of bool the carrier' of C
(C) . ( the of X \/ the of ExX) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ the of ExX)) is Element of bool the carrier' of C
the of X \/ ( the of X /\ the of X) is Element of bool the carrier' of C
(C) . ( the of X \/ ( the of X /\ the of X)) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ ( the of X /\ the of X))) is Element of bool the carrier' of C
(C) . the of X is Element of bool the carrier of C
(C) . ( the of X /\ the of X) is Element of bool the carrier of C
((C) . the of X) /\ ((C) . ( the of X /\ the of X)) is Element of bool the carrier of C
(C) . (((C) . the of X) /\ ((C) . ( the of X /\ the of X))) is Element of bool the carrier' of C
(C) . ((C) . the of X) is Element of bool the carrier' of C
(C) . the of X is Element of bool the carrier' of C
the of X /\ ((C) . ((C) . ( the of X \/ the of X))) is Element of bool the carrier of C
(C) . the of X is Element of bool the carrier' of C
((C) . the of X) /\ ((C) . the of X) is Element of bool the carrier' of C
(C) . (((C) . the of X) /\ ((C) . the of X)) is Element of bool the carrier of C
the of X /\ ((C) . (((C) . the of X) /\ ((C) . the of X))) is Element of bool the carrier of C
the of X /\ ((C) . the of X) is Element of bool the carrier' of C
(C) . ( the of X /\ ((C) . the of X)) is Element of bool the carrier of C
the of X /\ ((C) . ( the of X /\ ((C) . the of X))) is Element of bool the carrier of C
the of X /\ ((C) . ( the of X /\ the of X)) is Element of bool the carrier of C
ExX is Element of bool the carrier of C
E1 is Element of bool the carrier' of C
(C,ExX,E1) is (C) (C)
O is Element of bool the carrier of C
InX is Element of bool the carrier' of C
(C,O,InX) is (C) (C)
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is (C) (C) (C) (C) (C)
X is (C) (C) (C) (C)
(C) . (X,(C)) is set
[X,(C)] is V15() set
{X,(C)} is non empty set
{X} is non empty set
{{X,(C)},{X}} is non empty set
(C) . [X,(C)] is set
the of X is Element of bool the carrier of C
the of (C) is Element of bool the carrier of C
the of X /\ the of (C) is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
the of (C) is Element of bool the carrier' of C
the of X \/ the of (C) is Element of bool the carrier' of C
(C) . ( the of X \/ the of (C)) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ the of (C))) is Element of bool the carrier' of C
X is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,X,ExX) is (C) (C)
the of X /\ the carrier of C is Element of bool the carrier of C
(C) . the of 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
((C) . the of X) \/ ((C) . ExX) is Element of bool the carrier' of C
(C) . the of (C) is Element of bool the carrier' of C
the of X \/ ((C) . the of (C)) is Element of bool the carrier' of C
(C) . ( the of X \/ ((C) . the of (C))) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ ((C) . the of (C)))) is Element of bool the carrier' of C
(C) . the carrier of C is set
the of X \/ ((C) . the carrier of C) is set
(C) . ( the of X \/ ((C) . the carrier of C)) is set
(C) . ((C) . ( the of X \/ ((C) . the carrier of C))) is set
(C) . ((C) . the of X) is Element of bool the carrier of C
(C) . ((C) . ((C) . the of X)) is Element of bool the carrier' of C
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is (C) (C) (C) (C) (C)
X is (C) (C) (C) (C)
(C) . (X,(C)) is set
[X,(C)] is V15() set
{X,(C)} is non empty set
{X} is non empty set
{{X,(C)},{X}} is non empty set
(C) . [X,(C)] is set
the of X is Element of bool the carrier of C
the of (C) is Element of bool the carrier of C
the of X \/ the of (C) is Element of bool the carrier of C
(C) . ( the of X \/ the of (C)) is Element of bool the carrier' of C
(C) . ((C) . ( the of X \/ the of (C))) is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
the of (C) is Element of bool the carrier' of C
the of X /\ the of (C) is Element of bool the carrier' of C
X is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,X,ExX) is (C) (C)
the of X \/ the carrier of C is non empty set
(C) . ( the of X \/ the carrier of C) is set
(C) . ((C) . ( the of X \/ the carrier of C)) is set
(C) . the carrier of C is set
(C) . ((C) . the carrier of C) is set
(C) . the of (C) is Element of bool the carrier' of C
(C) . ((C) . the of (C)) is Element of bool the carrier of C
(C) . the of (C) is Element of bool the carrier of C
(C) . the of X is Element of bool the carrier' of C
((C) . the of X) /\ the of (C) is Element of bool the carrier' of C
((C) . the of X) /\ ((C) . the of (C)) is Element of bool the carrier' of C
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is (C) (C) (C) (C) (C)
X is (C) (C) (C) (C)
(C) . (X,(C)) is set
[X,(C)] is V15() set
{X,(C)} is non empty set
{X} is non empty set
{{X,(C)},{X}} is non empty set
(C) . [X,(C)] is set
the of X is Element of bool the carrier of C
the of (C) is Element of bool the carrier of C
the of X \/ the of (C) is Element of bool the carrier of C
(C) . ( the of X \/ the of (C)) is Element of bool the carrier' of C
(C) . ((C) . ( the of X \/ the of (C))) is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
the of (C) is Element of bool the carrier' of C
the of X /\ the of (C) is Element of bool the carrier' of C
X is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,X,ExX) is (C) (C)
the of X /\ the carrier' of C is Element of bool the carrier' of C
(C) . the of 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
((C) . the of X) \/ ((C) . ExX) is Element of bool the carrier of C
(C) . the of (C) is Element of bool the carrier of C
the of X \/ ((C) . the of (C)) is Element of bool the carrier of C
(C) . ( the of X \/ ((C) . the of (C))) is Element of bool the carrier' of C
(C) . ((C) . ( the of X \/ ((C) . the of (C)))) is Element of bool the carrier of C
(C) . the carrier' of C is set
the of X \/ ((C) . the carrier' of C) is set
(C) . ( the of X \/ ((C) . the carrier' of C)) is set
(C) . ((C) . ( the of X \/ ((C) . the carrier' of C))) is set
(C) . ((C) . the of X) is Element of bool the carrier' of C
(C) . ((C) . ((C) . the of X)) is Element of bool the carrier of C
C is () ()
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is (C) (C) (C) (C) (C)
X is (C) (C) (C) (C)
(C) . (X,(C)) is set
[X,(C)] is V15() set
{X,(C)} is non empty set
{X} is non empty set
{{X,(C)},{X}} is non empty set
(C) . [X,(C)] is set
the of X is Element of bool the carrier of C
the of (C) is Element of bool the carrier of C
the of X /\ the of (C) is Element of bool the carrier of C
the of X is Element of bool the carrier' of C
the of (C) is Element of bool the carrier' of C
the of X \/ the of (C) is Element of bool the carrier' of C
(C) . ( the of X \/ the of (C)) is Element of bool the carrier of C
(C) . ((C) . ( the of X \/ the of (C))) is Element of bool the carrier' of C
X is Element of bool the carrier of C
ExX is Element of bool the carrier' of C
(C,X,ExX) is (C) (C)
the of X \/ the carrier' of C is non empty set
(C) . ( the of X \/ the carrier' of C) is set
(C) . ((C) . ( the of X \/ the carrier' of C)) is set
(C) . the carrier' of C is set
(C) . ((C) . the carrier' of C) is set
(C) . the of (C) is Element of bool the carrier of C
(C) . ((C) . the of (C)) is Element of bool the carrier' of C
(C) . the of (C) is Element of bool the carrier' of C
(C) . the of X is Element of bool the carrier of C
((C) . the of X) /\ the of (C) is Element of bool the carrier of C
((C) . the of X) /\ ((C) . the of (C)) is Element of bool the carrier of C
C is () ()
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
LattStr(# (C),(C),(C) #) is non empty strict LattStr
C is () ()
(C) is non empty strict LattStr
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
LattStr(# (C),(C),(C) #) is non empty strict LattStr
X is non empty strict LattStr
the carrier of X is non empty set
ExX is Element of the carrier of X
ExX is Element of the carrier of X
E1 is Element of the carrier of X
ExX "\/" E1 is Element of the carrier of X
ExX "\/" (ExX "\/" E1) is Element of the carrier of X
ExX "\/" ExX is Element of the carrier of X
(ExX "\/" ExX) "\/" E1 is Element of the carrier of X
O is (C) (C) (C,(C))
InX is (C) (C) (C,(C))
(C) . (O,InX) is Element of (C)
[O,InX] is V15() set
{O,InX} is non empty set
{O} is non empty set
{{O,InX},{O}} is non empty set
(C) . [O,InX] is set
A9 is Element of the carrier of X
p is (C) (C) (C,(C))
p is (C) (C) (C,(C))
(C) . (p,p) is Element of (C)
[p,p] is V15() set
{p,p} is non empty set
{p} is non empty set
{{p,p},{p}} is non empty set
(C) . [p,p] is set
x is Element of the carrier of X
x9 is Element of the carrier of X
A is Element of the carrier of X
x9 "\/" A is Element of the carrier of X
x "\/" (x9 "\/" A) is Element of the carrier of X
In is Element of the carrier of X
x "\/" In is Element of the carrier of X
(C) . (x9,A) is set
[x9,A] is V15() set
{x9,A} is non empty set
{x9} is non empty set
{{x9,A},{x9}} is non empty set
(C) . [x9,A] is set
(C) . (x,((C) . (x9,A))) is set
[x,((C) . (x9,A))] is V15() set
{x,((C) . (x9,A))} is non empty set
{x} is non empty set
{{x,((C) . (x9,A))},{x}} is non empty set
(C) . [x,((C) . (x9,A))] is set
x "\/" x9 is Element of the carrier of X
(x "\/" x9) "\/" A is Element of the carrier of X
q is Element of the carrier of X
q "\/" A is Element of the carrier of X
(C) . (x,x9) is set
[x,x9] is V15() set
{x,x9} is non empty set
{{x,x9},{x}} is non empty set
(C) . [x,x9] is set
(C) . (((C) . (x,x9)),A) is set
[((C) . (x,x9)),A] is V15() set
{((C) . (x,x9)),A} is non empty set
{((C) . (x,x9))} is non empty set
{{((C) . (x,x9)),A},{((C) . (x,x9))}} is non empty set
(C) . [((C) . (x,x9)),A] is set
x is (C) (C) (C) (C)
x is (C) (C) (C) (C)
c is (C) (C) (C) (C)
(C) . (x,c) is set
[x,c] is V15() set
{x,c} is non empty set
{x} is non empty set
{{x,c},{x}} is non empty set
(C) . [x,c] is set
(C) . (x,((C) . (x,c))) is set
[x,((C) . (x,c))] is V15() set
{x,((C) . (x,c))} is non empty set
{x} is non empty set
{{x,((C) . (x,c))},{x}} is non empty set
(C) . [x,((C) . (x,c))] is set
(C) . (x,x) is set
[x,x] is V15() set
{x,x} is non empty set
{{x,x},{x}} is non empty set
(C) . [x,x] is set
(C) . (((C) . (x,x)),c) is set
[((C) . (x,x)),c] is V15() set
{((C) . (x,x)),c} is non empty set
{((C) . (x,x))} is non empty set
{{((C) . (x,x)),c},{((C) . (x,x))}} is non empty set
(C) . [((C) . (x,x)),c] is set
ExX is Element of the carrier of X
ExX is Element of the carrier of X
ExX "/\" ExX is Element of the carrier of X
(ExX "/\" ExX) "\/" ExX is Element of the carrier of X
E1 is (C) (C) (C,(C))
O is (C) (C) (C,(C))
(C) . (E1,O) is Element of (C)
[E1,O] is V15() set
{E1,O} is non empty set
{E1} is non empty set
{{E1,O},{E1}} is non empty set
(C) . [E1,O] is set
In is Element of the carrier of X
A9 is Element of the carrier of X
In "/\" A9 is Element of the carrier of X
(In "/\" A9) "\/" A9 is Element of the carrier of X
InX is Element of the carrier of X
InX "\/" A9 is Element of the carrier of X
(C) . (In,A9) is set
[In,A9] is V15() set
{In,A9} is non empty set
{In} is non empty set
{{In,A9},{In}} is non empty set
(C) . [In,A9] is set
(C) . (((C) . (In,A9)),A9) is set
[((C) . (In,A9)),A9] is V15() set
{((C) . (In,A9)),A9} is non empty set
{((C) . (In,A9))} is non empty set
{{((C) . (In,A9)),A9},{((C) . (In,A9))}} is non empty set
(C) . [((C) . (In,A9)),A9] is set
A is (C) (C) (C) (C)
p is (C) (C) (C) (C)
(C) . (A,p) is set
[A,p] is V15() set
{A,p} is non empty set
{A} is non empty set
{{A,p},{A}} is non empty set
(C) . [A,p] is set
(C) . (((C) . (A,p)),p) is set
[((C) . (A,p)),p] is V15() set
{((C) . (A,p)),p} is non empty set
{((C) . (A,p))} is non empty set
{{((C) . (A,p)),p},{((C) . (A,p))}} is non empty set
(C) . [((C) . (A,p)),p] is set
ExX is Element of the carrier of X
ExX is Element of the carrier of X
E1 is Element of the carrier of X
ExX "/\" E1 is Element of the carrier of X
ExX "/\" (ExX "/\" E1) is Element of the carrier of X
ExX "/\" ExX is Element of the carrier of X
(ExX "/\" ExX) "/\" E1 is Element of the carrier of X
O is (C) (C) (C,(C))
InX is (C) (C) (C,(C))
(C) . (O,InX) is Element of (C)
[O,InX] is V15() set
{O,InX} is non empty set
{O} is non empty set
{{O,InX},{O}} is non empty set
(C) . [O,InX] is set
A9 is Element of the carrier of X
A is Element of the carrier of X
A9 "/\" A is Element of the carrier of X
ExX "/\" (A9 "/\" A) is Element of the carrier of X
In is Element of the carrier of X
ExX "/\" In is Element of the carrier of X
(C) . (A9,A) is set
[A9,A] is V15() set
{A9,A} is non empty set
{A9} is non empty set
{{A9,A},{A9}} is non empty set
(C) . [A9,A] is set
(C) . (ExX,((C) . (A9,A))) is set
[ExX,((C) . (A9,A))] is V15() set
{ExX,((C) . (A9,A))} is non empty set
{ExX} is non empty set
{{ExX,((C) . (A9,A))},{ExX}} is non empty set
(C) . [ExX,((C) . (A9,A))] is set
p is (C) (C) (C,(C))
p is (C) (C) (C,(C))
(C) . (p,p) is Element of (C)
[p,p] is V15() set
{p,p} is non empty set
{p} is non empty set
{{p,p},{p}} is non empty set
(C) . [p,p] is set
x is Element of the carrier of X
x9 is Element of the carrier of X
x "/\" x9 is Element of the carrier of X
(x "/\" x9) "/\" A is Element of the carrier of X
q is Element of the carrier of X
q "/\" A is Element of the carrier of X
(C) . (x,x9) is set
[x,x9] is V15() set
{x,x9} is non empty set
{x} is non empty set
{{x,x9},{x}} is non empty set
(C) . [x,x9] is set
(C) . (((C) . (x,x9)),A) is set
[((C) . (x,x9)),A] is V15() set
{((C) . (x,x9)),A} is non empty set
{((C) . (x,x9))} is non empty set
{{((C) . (x,x9)),A},{((C) . (x,x9))}} is non empty set
(C) . [((C) . (x,x9)),A] is set
x is (C) (C) (C) (C)
x is (C) (C) (C) (C)
c is (C) (C) (C) (C)
(C) . (x,c) is set
[x,c] is V15() set
{x,c} is non empty set
{x} is non empty set
{{x,c},{x}} is non empty set
(C) . [x,c] is set
(C) . (x,((C) . (x,c))) is set
[x,((C) . (x,c))] is V15() set
{x,((C) . (x,c))} is non empty set
{x} is non empty set
{{x,((C) . (x,c))},{x}} is non empty set
(C) . [x,((C) . (x,c))] is set
(C) . (x,x) is set
[x,x] is V15() set
{x,x} is non empty set
{{x,x},{x}} is non empty set
(C) . [x,x] is set
(C) . (((C) . (x,x)),c) is set
[((C) . (x,x)),c] is V15() set
{((C) . (x,x)),c} is non empty set
{((C) . (x,x))} is non empty set
{{((C) . (x,x)),c},{((C) . (x,x))}} is non empty set
(C) . [((C) . (x,x)),c] is set
ExX is Element of the carrier of X
ExX is Element of the carrier of X
ExX "/\" ExX is Element of the carrier of X
ExX "/\" ExX is Element of the carrier of X
(C) . (ExX,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
(C) . [ExX,ExX] is set
E1 is (C) (C) (C) (C)
O is (C) (C) (C) (C)
(C) . (E1,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
(C) . [E1,O] is set
(C) . (O,E1) is set
[O,E1] is V15() set
{O,E1} is non empty set
{O} is non empty set
{{O,E1},{O}} is non empty set
(C) . [O,E1] is set
ExX is Element of the carrier of X
ExX is Element of the carrier of X
ExX "\/" ExX is Element of the carrier of X
ExX "/\" (ExX "\/" ExX) is Element of the carrier of X
E1 is (C) (C) (C,(C))
O is (C) (C) (C,(C))
(C) . (E1,O) is Element of (C)
[E1,O] is V15() set
{E1,O} is non empty set
{E1} is non empty set
{{E1,O},{E1}} is non empty set
(C) . [E1,O] is set
In is Element of the carrier of X
A9 is Element of the carrier of X
In "\/" A9 is Element of the carrier of X
In "/\" (In "\/" A9) is Element of the carrier of X
InX is Element of the carrier of X
In "/\" InX is Element of the carrier of X
(C) . (In,A9) is set
[In,A9] is V15() set
{In,A9} is non empty set
{In} is non empty set
{{In,A9},{In}} is non empty set
(C) . [In,A9] is set
(C) . (In,((C) . (In,A9))) is set
[In,((C) . (In,A9))] is V15() set
{In,((C) . (In,A9))} is non empty set
{{In,((C) . (In,A9))},{In}} is non empty set
(C) . [In,((C) . (In,A9))] is set
A is (C) (C) (C) (C)
p is (C) (C) (C) (C)
(C) . (A,p) is set
[A,p] is V15() set
{A,p} is non empty set
{A} is non empty set
{{A,p},{A}} is non empty set
(C) . [A,p] is set
(C) . (A,((C) . (A,p))) is set
[A,((C) . (A,p))] is V15() set
{A,((C) . (A,p))} is non empty set
{{A,((C) . (A,p))},{A}} is non empty set
(C) . [A,((C) . (A,p))] is set
ExX is Element of the carrier of X
ExX is Element of the carrier of X
ExX "\/" ExX is Element of the carrier of X
ExX "\/" ExX is Element of the carrier of X
(C) . (ExX,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
(C) . [ExX,ExX] is set
E1 is (C) (C) (C) (C)
O is (C) (C) (C) (C)
(C) . (E1,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
(C) . [E1,O] is set
(C) . (O,E1) is set
[O,E1] is V15() set
{O,E1} is non empty set
{O} is non empty set
{{O,E1},{O}} is non empty set
(C) . [O,E1] is set
C is () ()
(C) is non empty strict LattStr
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
LattStr(# (C),(C),(C) #) is non empty strict LattStr
C is () ()
(C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
LattStr(# (C),(C),(C) #) is non empty strict LattStr
the carrier of (C) is non empty set
bool the carrier of (C) is non empty set
X is non empty Element of bool the carrier of (C)
X is Element of X
C is () ()
(C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
LattStr(# (C),(C),(C) #) is non empty strict LattStr
the carrier of (C) is non empty set
X is Element of the carrier of (C)
C is () ()
(C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
LattStr(# (C),(C),(C) #) is non empty strict LattStr
the carrier of (C) is non empty set
X is Element of the carrier of (C)
X is Element of the carrier of (C)
(C,X) is (C) (C) (C) (C)
(C,X) is (C) (C) (C) (C)
the of (C,X) is Element of bool the carrier' of C
the of (C,X) is Element of bool the carrier' of C
the of (C,X) /\ the of (C,X) is Element of bool the carrier' of C
(C) . ((C,X),(C,X)) is set
[(C,X),(C,X)] is V15() set
{(C,X),(C,X)} is non empty set
{(C,X)} is non empty set
{{(C,X),(C,X)},{(C,X)}} is non empty set
(C) . [(C,X),(C,X)] is set
the of (C,X) is Element of bool the carrier of C
the of (C,X) is Element of bool the carrier of C
the of (C,X) \/ the of (C,X) is Element of bool the carrier of C
(C) . ( the of (C,X) \/ the of (C,X)) is Element of bool the carrier' of C
(C) . ((C) . ( the of (C,X) \/ the of (C,X))) is Element of bool the carrier of C
ExX is Element of bool the carrier of C
E1 is Element of bool the carrier' of C
(C,ExX,E1) is (C) (C)
(C) . the of (C,X) is Element of bool the carrier of C
X "\/" X is Element of the carrier of (C)
the L_join of (C) is Relation-like [: the carrier of (C), the carrier of (C):] -defined the carrier of (C) -valued Function-like non empty V14([: the carrier of (C), the carrier of (C):]) V18([: the carrier of (C), 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), the carrier of (C):] is non empty set
[:[: 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):], the carrier of (C):] is non empty set
the L_join of (C) . (X,X) is Element of the carrier of (C)
[X,X] is V15() set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
the L_join of (C) . [X,X] is set
ExX is set
E1 is Element of bool the carrier of C
O is Element of bool the carrier' of C
(C,E1,O) is (C) (C)
C is () ()
(C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
LattStr(# (C),(C),(C) #) is non empty strict LattStr
the carrier of (C) is non empty set
bool the carrier of (C) is non empty set
X is Element of bool the carrier of (C)
Top (C) is Element of the carrier of (C)
X is Element of the carrier of (C)
(C) is (C) (C) (C) (C) (C)
ExX is Element of the carrier of (C)
ExX is Element of the carrier of (C)
ExX "\/" ExX is Element of the carrier of (C)
ExX "\/" ExX is Element of the carrier of (C)
O is (C) (C) (C) (C)
E1 is (C) (C) (C) (C)
(C) . (O,E1) is set
[O,E1] is V15() set
{O,E1} is non empty set
{O} is non empty set
{{O,E1},{O}} is non empty set
(C) . [O,E1] is set
(C) . (E1,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
(C) . [E1,O] is set
ExX is Element of the carrier of (C)
(Top (C)) "\/" X is Element of the carrier of (C)
X is Element of the carrier of (C)
X is non empty Element of bool the carrier of (C)
{ the of b₁ where b₁ is (C) (C) (C,(C)) : b₁ in X } is set
ExX is (C) (C) (C,X)
the of ExX is Element of bool the carrier of C
E1 is (C) (C) (C,(C))
the of E1 is Element of bool the carrier of C
ExX is non empty set
meet ExX is set
O is Element of the carrier of C
InX is set
In is (C) (C) (C,(C))
the of In is Element of bool the carrier of C
InX is (C) (C) (C,X)
the of InX is Element of bool the carrier of C
InX is (C) (C) (C,X)
the of InX is Element of bool the carrier of C
In is (C) (C) (C,X)
the of In is Element of bool the carrier of C
the Element of ExX is Element of ExX
InX is set
In is (C) (C) (C,(C))
the of In is Element of bool the carrier of C
O is Element of bool the carrier of C
{ the of b₁ where b₁ is (C) (C) (C,(C)) : b₁ in X } is set
union { the of b₁ where b₁ is (C) (C) (C,(C)) : b₁ in X } is set
A9 is Element of the carrier' of C
A is (C) (C) (C,X)
the of A is Element of bool the carrier' of C
A is (C) (C) (C,X)
the of A is Element of bool the carrier' of C
A is set
A is set
p is (C) (C) (C,(C))
the of p is Element of bool the carrier' of C
A is (C) (C) (C,X)
the of A is Element of bool the carrier' of C
p is (C) (C) (C,X)
the of p is Element of bool the carrier' of C
A9 is set
A is set
p is (C) (C) (C,(C))
the of p is Element of bool the carrier' of C
A9 is Element of bool the carrier' of C
A is Element of the carrier of C
p is (C) (C) (C,X)
the of p is Element of bool the carrier of C
the of p is Element of bool the carrier' of C
(C) . the of p is Element of bool the carrier of C
p is (C) (C) (C,X)
the of p is Element of bool the carrier' of C
(C) . the of p is Element of bool the carrier of C
the of p is Element of bool the carrier of C
p is (C) (C) (C,X)
the of p is Element of bool the carrier' of C
(C) . the of p is Element of bool the carrier of C
p is (C) (C) (C,X)
the of p is Element of bool the carrier' of C
(C) . the of p is Element of bool the carrier of C
p is (C) (C) (C,X)
the of p is Element of bool the carrier' of C
(C) . the of p is Element of bool the carrier of C
(C) . A9 is Element of bool the carrier of C
A is set
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in A9 or not (C,b₁,b₂) ) } is set
p is Element of the carrier of C
p is (C) (C) (C,X)
the of p is Element of bool the carrier' of C
(C) . the of p is Element of bool the carrier of C
q is Element of the carrier' of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in the of p or not (C,b₁,b₂) ) } is set
(C) . ((C) . A9) is Element of bool the carrier' of C
A is Element of bool the carrier' of C
(C,O,A) is (C) (C)
p is set
q is Element of the carrier of C
x is Element of the carrier' of C
x9 is (C) (C) (C,X)
the of x9 is Element of bool the carrier' of C
(C) . the of x9 is Element of bool the carrier of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in the of x9 or not (C,b₁,b₂) ) } is set
x is Element of the carrier of C
{ b₁ where b₁ is Element of the carrier of C : for b₂ being Element of the carrier' of C holds
( not b₂ in A9 or not (C,b₁,b₂) ) } is set
p is Element of the carrier of (C)
q is Element of the carrier of (C)
(C,q) is (C) (C) (C) (C)
the of (C,q) is Element of bool the carrier of C
(C,p) is (C) (C) (C) (C)
the of (C,p) is Element of bool the carrier of C
x is set
x9 is Element of the carrier of C
x is (C) (C) (C,X)
the of x is Element of bool the carrier of C
x is Element of the carrier of (C)
(C,x) is (C) (C) (C) (C)
the of (C,x) is Element of bool the carrier of C
q is Element of the carrier of (C)
(C,p) is (C) (C) (C) (C)
the of (C,p) is Element of bool the carrier of C
(C,q) is (C) (C) (C) (C)
the of (C,q) is Element of bool the carrier of C
x is set
C is () ()
(C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(C) is non empty (C)
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
{ (C,b₁,b₂) where b₁ is Element of bool the carrier of C, b₂ is Element of bool the carrier' of C : ( (C,b₁,b₂) is (C) & (C) . b₁ = b₂ & (C) . b₂ = b₁ ) } is set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
[:(C),(C):] is non empty set
[:[:(C),(C):],(C):] is non empty set
bool [:[:(C),(C):],(C):] is non empty set
(C) is Relation-like [:(C),(C):] -defined (C) -valued Function-like non empty V14([:(C),(C):]) V18([:(C),(C):],(C)) Element of bool [:[:(C),(C):],(C):]
LattStr(# (C),(C),(C) #) is non empty strict LattStr