:: ORDERS_2 semantic presentation

K116() is non empty V34() V35() V36() V41() cardinal limit_cardinal set
bool K116() is non empty V41() set
{} is empty V34() V35() V36() V38() V39() V40() V41() cardinal {} -element set
the empty V34() V35() V36() V38() V39() V40() V41() cardinal {} -element set is empty V34() V35() V36() V38() V39() V40() V41() cardinal {} -element set
1 is non empty V34() V35() V36() V40() V41() cardinal Element of K116()
R is non empty set
[:R,R:] is non empty set
bool [:R,R:] is non empty set

(R,X) is () ()
is non empty trivial 1 -element set
is non empty set
bool is non empty set

X is non empty () ()

() \/ () is set
the carrier of X is non empty set
the of X is Relation-like the carrier of X -defined the carrier of X -valued 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
R is ()
the of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is set
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
dom the of R is Element of bool the carrier of R
bool the carrier of R is non empty set
R is () ()
the carrier of R is set
the of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
R is () () ()
the of R is Relation-like the carrier of R -defined the carrier of R -valued total Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is set
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
field the of R is set
dom the of R is set
rng the of R is set
(dom the of R) \/ (rng the of R) is set
R is () () ()
the of R is Relation-like the carrier of R -defined the carrier of R -valued total Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is set
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
field the of R is set
dom the of R is set
rng the of R is set
(dom the of R) \/ (rng the of R) is set
R is () () ()
the of R is Relation-like the carrier of R -defined the carrier of R -valued total Element of bool [: the carrier of R, the carrier of R:]
the carrier of R is set
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
field the of R is set
dom the of R is set
rng the of R is set
(dom the of R) \/ (rng the of R) is set
R is set
[:R,R:] is set
bool [:R,R:] is non empty set

(R,X) is () ()
field X is set
dom X is set
rng X is set
(dom X) \/ (rng X) is set
the of (R,X) is Relation-like the carrier of (R,X) -defined the carrier of (R,X) -valued Element of bool [: the carrier of (R,X), the carrier of (R,X):]
the carrier of (R,X) is set
[: the carrier of (R,X), the carrier of (R,X):] is set
bool [: the carrier of (R,X), the carrier of (R,X):] is non empty set
R is set
[:R,R:] is set
bool [:R,R:] is non empty set

(R,X) is () ()
field X is set
dom X is set
rng X is set
(dom X) \/ (rng X) is set
the of (R,X) is Relation-like the carrier of (R,X) -defined the carrier of (R,X) -valued Element of bool [: the carrier of (R,X), the carrier of (R,X):]
the carrier of (R,X) is set
[: the carrier of (R,X), the carrier of (R,X):] is set
bool [: the carrier of (R,X), the carrier of (R,X):] is non empty set
R is set
[:R,R:] is set
bool [:R,R:] is non empty set

(R,X) is () ()
field X is set
dom X is set
rng X is set
(dom X) \/ (rng X) is set
the of (R,X) is Relation-like the carrier of (R,X) -defined the carrier of (R,X) -valued Element of bool [: the carrier of (R,X), the carrier of (R,X):]
the carrier of (R,X) is set
[: the carrier of (R,X), the carrier of (R,X):] is set
bool [: the carrier of (R,X), the carrier of (R,X):] is non empty set
X is non empty () () () () ()
the carrier of X is non empty set
bool the carrier of X is non empty set
R is set
R is Element of bool the carrier of X
R is ()
the carrier of R is set
R is ()
the carrier of R is set
R is ()
the carrier of R is set
R is Element of the carrier of R
R is ()
the carrier of R is set
R is non empty () () ()
the carrier of R is non empty set
X is Element of the carrier of R
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
[X,X] is Element of [: the carrier of R, the carrier of R:]
{X,X} is non empty set
{X} is non empty trivial 1 -element set
{{X,X},{X}} is non empty set
R is non empty () () ()
the carrier of R is non empty set
R is Element of the carrier of R
R is () ()
the carrier of R is set
X is Element of the carrier of R
R is Element of the carrier of R
[X,R] is set
{X,R} is non empty set
{X} is non empty trivial 1 -element set
{{X,R},{X}} is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
[R,X] is set
{R,X} is non empty set
{R} is non empty trivial 1 -element set
{{R,X},{R}} is non empty set
R is () ()
the carrier of R is set
X is Element of the carrier of R
R is Element of the carrier of R
R is Element of the carrier of R
[X,R] is set
{X,R} is non empty set
{X} is non empty trivial 1 -element set
{{X,R},{X}} is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
[R,R] is set
{R,R} is non empty set
{R} is non empty trivial 1 -element set
{{R,R},{R}} is non empty set
[X,R] is set
{X,R} is non empty set
{{X,R},{X}} is non empty set
R is () ()
the carrier of R is set
X is Element of the carrier of R
R is Element of the carrier of R
R is () () ()
the carrier of R is set
X is Element of the carrier of R
R is Element of the carrier of R
R is Element of the carrier of R
R is () ()
the carrier of R is set
X is Element of the carrier of R
R is Element of the carrier of R
R is () () ()
the carrier of R is set
X is Element of the carrier of R
R is Element of the carrier of R
R is Element of the carrier of R
R is ()
the carrier of R is set
bool the carrier of R is non empty set
R is ()
the carrier of R is set
bool the carrier of R is non empty set
X is Element of bool the carrier of R
{} R is empty V34() V35() V36() V38() V39() V40() V41() cardinal {} -element Element of bool the carrier of R
R is set
R is set
[R,R] is set
{R,R} is non empty set
{R} is non empty trivial 1 -element set
{{R,R},{R}} is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
[R,R] is set
{R,R} is non empty set
{R} is non empty trivial 1 -element set
{{R,R},{R}} is non empty set
R is ()
the carrier of R is set
bool the carrier of R is non empty set
{} R is empty V34() V35() V36() V38() V39() V40() V41() cardinal {} -element (R) Element of bool the carrier of R
R is non empty () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of the carrier of R
{X} is non empty trivial 1 -element Element of bool the carrier of R
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
R is set
R is set
[R,R] is set
{R,R} is non empty set
{R} is non empty trivial 1 -element set
{{R,R},{R}} is non empty set
[R,R] is set
{R,R} is non empty set
{R} is non empty trivial 1 -element set
{{R,R},{R}} is non empty set
R is non empty () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of the carrier of R
R is Element of the carrier of R
{X,R} is non empty Element of bool the carrier of R
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
[X,R] is Element of [: the carrier of R, the carrier of R:]
{X,R} is non empty set
{X} is non empty trivial 1 -element set
{{X,R},{X}} is non empty set
[R,X] is Element of [: the carrier of R, the carrier of R:]
{R,X} is non empty set
{R} is non empty trivial 1 -element set
{{R,X},{R}} is non empty set
R is set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
B is set
[R,B] is set
{R,B} is non empty set
{R} is non empty trivial 1 -element set
{{R,B},{R}} is non empty set
[B,R] is set
{B,R} is non empty set
{B} is non empty trivial 1 -element set
{{B,R},{B}} is non empty set
R is ()
the carrier of R is set
bool the carrier of R is non empty set
X is (R) Element of bool the carrier of R
R is Element of bool the carrier of R
the of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
R is () () ()
the carrier of R is set
bool the carrier of R is non empty set
X is Element of the carrier of R
R is Element of the carrier of R
R is (R) Element of bool the carrier of R
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
[X,R] is set
{X,R} is non empty set
{X} is non empty trivial 1 -element set
{{X,R},{X}} is non empty set
[R,X] is set
{R,X} is non empty set
{R} is non empty trivial 1 -element set
{{R,X},{R}} is non empty set
[X,R] is set
{X,R} is non empty set
{X} is non empty trivial 1 -element set
{{X,R},{X}} is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
[R,X] is set
{R,X} is non empty set
{R} is non empty trivial 1 -element set
{{R,X},{R}} is non empty set
R is non empty () () ()
the carrier of R is non empty set
B is Element of the carrier of R
e is Element of the carrier of R
{B,e} is non empty Element of bool the carrier of R
bool the carrier of R is non empty set
d is (R) Element of bool the carrier of R
R is () () () ()
the carrier of R is set
bool the carrier of R is non empty set
X is Element of the carrier of R
R is Element of the carrier of R
R is (R) Element of bool the carrier of R
R is ()
the carrier of R is set
bool the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is set
bool [: the carrier of R, the carrier of R:] is non empty set
X is Element of bool the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in X or not (R,b2,b1) )
}
is set

R is set
B is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in X or not (R,b1,b2) )
}
is set

R is set
B is Element of the carrier of R
R is non empty () () () () ()
{} R is empty proper V34() V35() V36() V38() V39() V40() V41() cardinal {} -element (R) Element of bool the carrier of R
the carrier of R is non empty set
bool the carrier of R is non empty set
(R,({} R)) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {} R or not (R,b2,b1) )
}
is set

X is set
R is Element of the carrier of R
R is Element of the carrier of R
R is non empty () () () () ()
[#] R is non empty non proper Element of bool the carrier of R
the carrier of R is non empty set
bool the carrier of R is non empty set
(R,([#] R)) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in [#] R or not (R,b2,b1) )
}
is set

X is set
R is Element of the carrier of R
R is non empty () () () () ()
{} R is empty proper V34() V35() V36() V38() V39() V40() V41() cardinal {} -element (R) Element of bool the carrier of R
the carrier of R is non empty set
bool the carrier of R is non empty set
(R,({} R)) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {} R or not (R,b1,b2) )
}
is set

X is set
R is Element of the carrier of R
R is Element of the carrier of R
R is non empty () () () () ()
[#] R is non empty non proper Element of bool the carrier of R
the carrier of R is non empty set
bool the carrier of R is non empty set
(R,([#] R)) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in [#] R or not (R,b1,b2) )
}
is set

X is set
R is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of the carrier of R
R is Element of bool the carrier of R
(R,R) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in R or not (R,b2,b1) )
}
is set

R is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
X is Element of the carrier of R
{X} is non empty trivial 1 -element Element of bool the carrier of R
bool the carrier of R is non empty set
(R,{X}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {X} or not (R,b2,b1) )
}
is set

R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of the carrier of R
R is Element of bool the carrier of R
(R,R) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in R or not (R,b1,b2) )
}
is set

R is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
X is Element of the carrier of R
{X} is non empty trivial 1 -element Element of bool the carrier of R
bool the carrier of R is non empty set
(R,{X}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {X} or not (R,b1,b2) )
}
is set

R is non empty () () () () ()
the carrier of R is non empty set
X is Element of the carrier of R
{X} is non empty trivial 1 -element Element of bool the carrier of R
bool the carrier of R is non empty set
(R,{X}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {X} or not (R,b2,b1) )
}
is set

R is Element of the carrier of R
R is Element of the carrier of R
R is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
X is Element of the carrier of R
R is Element of the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
bool the carrier of R is non empty set
(R,{R}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {R} or not (R,b1,b2) )
}
is set

R is Element of the carrier of R
R is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
R is Element of the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
(R,{R}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {R} or not (R,b1,b2) )
}
is set

X is Element of bool the carrier of R
(R,{R}) /\ X is Element of bool the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of bool the carrier of R
the Element of X is Element of X
R is Element of the carrier of R
(R,X,R) is Element of bool the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
(R,{R}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {R} or not (R,b1,b2) )
}
is set

(R,{R}) /\ X is Element of bool the carrier of R
B is Element of bool the carrier of R
R is Element of the carrier of R
R is Element of bool the carrier of R
(R,X,R) is Element of bool the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
(R,{R}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {R} or not (R,b1,b2) )
}
is set

(R,{R}) /\ X is Element of bool the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of the carrier of R
R is Element of the carrier of R
R is Element of bool the carrier of R
(R,R,R) is Element of bool the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
(R,{R}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {R} or not (R,b1,b2) )
}
is set

(R,{R}) /\ R is Element of bool the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
{} R is empty proper V34() V35() V36() V38() V39() V40() V41() cardinal {} -element (R) Element of bool the carrier of R
bool the carrier of R is non empty set
X is Element of the carrier of R
(R,({} R),X) is Element of bool the carrier of R
{X} is non empty trivial 1 -element Element of bool the carrier of R
(R,{X}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {X} or not (R,b1,b2) )
}
is set

(R,{X}) /\ ({} R) is Element of bool the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of the carrier of R
R is Element of bool the carrier of R
(R,R,X) is Element of bool the carrier of R
{X} is non empty trivial 1 -element Element of bool the carrier of R
(R,{X}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {X} or not (R,b1,b2) )
}
is set

(R,{X}) /\ R is Element of bool the carrier of R
R is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of the carrier of R
R is Element of the carrier of R
R is Element of bool the carrier of R
(R,R,X) is Element of bool the carrier of R
{X} is non empty trivial 1 -element Element of bool the carrier of R
(R,{X}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {X} or not (R,b1,b2) )
}
is set

(R,{X}) /\ R is Element of bool the carrier of R
(R,R,R) is Element of bool the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
(R,{R}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {R} or not (R,b1,b2) )
}
is set

(R,{R}) /\ R is Element of bool the carrier of R
B is set
e is Element of the carrier of R
d is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of the carrier of R
R is Element of bool the carrier of R
(R,R,X) is Element of bool the carrier of R
{X} is non empty trivial 1 -element Element of bool the carrier of R
(R,{X}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {X} or not (R,b1,b2) )
}
is set

(R,{X}) /\ R is Element of bool the carrier of R
R is Element of bool the carrier of R
(R,R,X) is Element of bool the carrier of R
(R,{X}) /\ R is Element of bool the carrier of R
B is set
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of bool the carrier of R
R is (R,X)
R is Element of the carrier of R
(R,X,R) is Element of bool the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
(R,{R}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {R} or not (R,b1,b2) )
}
is set

(R,{R}) /\ X is Element of bool the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of bool the carrier of R
R is Element of the carrier of R
(R,X,R) is Element of bool the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
(R,{R}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {R} or not (R,b1,b2) )
}
is set

(R,{R}) /\ X is Element of bool the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of bool the carrier of R
R is Element of bool the carrier of R
R is Element of the carrier of R
(R,R,R) is Element of bool the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
(R,{R}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {R} or not (R,b1,b2) )
}
is set

(R,{R}) /\ R is Element of bool the carrier of R
B is Element of the carrier of R
(R,X,B) is Element of bool the carrier of R
{B} is non empty trivial 1 -element Element of bool the carrier of R
(R,{B}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {B} or not (R,b1,b2) )
}
is set

(R,{B}) /\ X is Element of bool the carrier of R
e is Element of the carrier of R
e is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of the carrier of R
R is Element of the carrier of R
R is Element of bool the carrier of R
B is Element of bool the carrier of R
e is Element of the carrier of R
(R,R,e) is Element of bool the carrier of R
{e} is non empty trivial 1 -element Element of bool the carrier of R
(R,{e}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {e} or not (R,b1,b2) )
}
is set

(R,{e}) /\ R is Element of bool the carrier of R
d is Element of the carrier of R
b is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
X is Element of the carrier of R
R is Element of bool the carrier of R
(R,R,X) is Element of bool the carrier of R
{X} is non empty trivial 1 -element Element of bool the carrier of R
(R,{X}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {X} or not (R,b1,b2) )
}
is set

(R,{X}) /\ R is Element of bool the carrier of R
R is Element of bool the carrier of R
(R,R,X) is Element of bool the carrier of R
(R,{X}) /\ R is Element of bool the carrier of R
B is set
B is set
e is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is Element of bool the carrier of R
R is Element of bool the carrier of R
R \ X is Element of bool the carrier of R
B is set
e is Element of the carrier of R
(R,R,e) is Element of bool the carrier of R
{e} is non empty trivial 1 -element Element of bool the carrier of R
(R,{e}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {e} or not (R,b1,b2) )
}
is set

(R,{e}) /\ R is Element of bool the carrier of R
d is set
f is Element of the carrier of R
b is Element of the carrier of R
d is set
b is Element of the carrier of R
[e,d] is set
{e,d} is non empty set
{e} is non empty trivial 1 -element set
{{e,d},{e}} is non empty set
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is Element of bool the carrier of R
R is Element of bool the carrier of R
R \ X is Element of bool the carrier of R
B is set
e is Element of the carrier of R
(R,R,e) is Element of bool the carrier of R
{e} is non empty trivial 1 -element Element of bool the carrier of R
(R,{e}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {e} or not (R,b1,b2) )
}
is set

(R,{e}) /\ R is Element of bool the carrier of R
d is set
f is Element of the carrier of R
b is Element of the carrier of R
d is set
b is Element of the carrier of R
[e,d] is set
{e,d} is non empty set
{e} is non empty trivial 1 -element set
{{e,d},{e}} is non empty set
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
is non empty trivial 1 -element set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
X . the carrier of R is set
R is Element of the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
B is (R) Element of bool the carrier of R
d is set
e is set
the of R -Seg e is set
Coim ( the of R,e) is set
{e} is non empty trivial 1 -element set
the of R " {e} is set
(Coim ( the of R,e)) \ {e} is Element of bool (Coim ( the of R,e))
bool (Coim ( the of R,e)) is non empty set
( the of R -Seg e) /\ d is set
b is set
e is Element of the carrier of R
(R,B,e) is Element of bool the carrier of R
{e} is non empty trivial 1 -element Element of bool the carrier of R
(R,{e}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {e} or not (R,b1,b2) )
}
is set

(R,{e}) /\ B is Element of bool the carrier of R
(R,(R,B,e)) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in (R,B,e) or not (R,b2,b1) )
}
is set

X . (R,(R,B,e)) is set
{} R is empty proper V34() V35() V36() V38() V39() V40() V41() cardinal {} -element (R) Element of bool the carrier of R
d is set
b is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
X . the carrier of R is set
{(X . the carrier of R)} is non empty trivial 1 -element set
R is Element of the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
B is (R) Element of bool the carrier of R
d is set
e is set
the of R -Seg e is set
Coim ( the of R,e) is set
{e} is non empty trivial 1 -element set
the of R " {e} is set
(Coim ( the of R,e)) \ {e} is Element of bool (Coim ( the of R,e))
bool (Coim ( the of R,e)) is non empty set
( the of R -Seg e) /\ d is set
b is set
e is Element of the carrier of R
(R,B,e) is Element of bool the carrier of R
{e} is non empty trivial 1 -element Element of bool the carrier of R
(R,{e}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {e} or not (R,b1,b2) )
}
is set

(R,{e}) /\ B is Element of bool the carrier of R
(R,(R,B,e)) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in (R,B,e) or not (R,b2,b1) )
}
is set

X . (R,(R,B,e)) is set
{} R is empty proper V34() V35() V36() V38() V39() V40() V41() cardinal {} -element (R) Element of bool the carrier of R
d is set
b is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
X . the carrier of R is set
R is (R) (R,X)
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
R is set
B is Element of the carrier of R
{B} is non empty trivial 1 -element Element of bool the carrier of R
(R,{B}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {B} or not (R,b1,b2) )
}
is set

(R,{B}) /\ R is Element of bool the carrier of R
the Element of (R,{B}) /\ R is Element of (R,{B}) /\ R
{} R is empty proper V34() V35() V36() V38() V39() V40() V41() cardinal {} -element (R) Element of bool the carrier of R
d is Element of the carrier of R
[B, the Element of (R,{B}) /\ R] is set
{B, the Element of (R,{B}) /\ R} is non empty set
{B} is non empty trivial 1 -element set
{{B, the Element of (R,{B}) /\ R},{B}} is non empty set
b is Element of the carrier of R
(R,R,B) is Element of bool the carrier of R
(R,((R,{B}) /\ R)) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in (R,{B}) /\ R or not (R,b2,b1) )
}
is set

X . (R,((R,{B}) /\ R)) is set
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Element of the carrier of R
R is Element of the carrier of R
R is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
R . the carrier of R is set
B is (R) (R,R)
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
e is set
d is Element of the carrier of R
{d} is non empty trivial 1 -element Element of bool the carrier of R
(R,{d}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {d} or not (R,b1,b2) )
}
is set

(R,{d}) /\ B is Element of bool the carrier of R
the Element of (R,{d}) /\ B is Element of (R,{d}) /\ B
{} R is empty proper V34() V35() V36() V38() V39() V40() V41() cardinal {} -element (R) Element of bool the carrier of R
f is Element of the carrier of R
[d, the Element of (R,{d}) /\ B] is set
{d, the Element of (R,{d}) /\ B} is non empty set
{d} is non empty trivial 1 -element set
{{d, the Element of (R,{d}) /\ B},{d}} is non empty set
e is Element of the carrier of R
(R,B,d) is Element of bool the carrier of R
(R,((R,{d}) /\ B)) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in (R,{d}) /\ B or not (R,b2,b1) )
}
is set

R . (R,((R,{d}) /\ B)) is set
[d,X] is Element of [: the carrier of R, the carrier of R:]
{d,X} is non empty set
{{d,X},{d}} is non empty set
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Element of the carrier of R
R is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
R . the carrier of R is set
R is (R) (R,R)
(R,R,X) is Element of bool the carrier of R
{X} is non empty trivial 1 -element Element of bool the carrier of R
(R,{X}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {X} or not (R,b1,b2) )
}
is set

(R,{X}) /\ R is Element of bool the carrier of R
the Element of (R,{X}) /\ R is Element of (R,{X}) /\ R
e is Element of the carrier of R
d is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
R is (R) (R,X)
R is (R) (R,X)
X . the carrier of R is set
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
R is (R) (R,X)
R is (R) (R,X)
R /\ R is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : ( b1 in R /\ R & (R,R,b1) = (R,R,b1) ) } is set
e is set
d is Element of the carrier of R
(R,R,d) is Element of bool the carrier of R
{d} is non empty trivial 1 -element Element of bool the carrier of R
(R,{d}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {d} or not (R,b1,b2) )
}
is set

(R,{d}) /\ R is Element of bool the carrier of R
(R,R,d) is Element of bool the carrier of R
(R,{d}) /\ R is Element of bool the carrier of R
e is Element of bool the carrier of R
d is set
b is Element of the carrier of R
(R,R,b) is Element of bool the carrier of R
{b} is non empty trivial 1 -element Element of bool the carrier of R
(R,{b}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {b} or not (R,b1,b2) )
}
is set

(R,{b}) /\ R is Element of bool the carrier of R
(R,R,b) is Element of bool the carrier of R
(R,{b}) /\ R is Element of bool the carrier of R
b is Element of the carrier of R
d is Element of the carrier of R
(R,R,d) is Element of bool the carrier of R
{d} is non empty trivial 1 -element Element of bool the carrier of R
(R,{d}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {d} or not (R,b1,b2) )
}
is set

(R,{d}) /\ R is Element of bool the carrier of R
(R,R,d) is Element of bool the carrier of R
(R,{d}) /\ R is Element of bool the carrier of R
f is set
e is Element of the carrier of R
(R,R,b) is Element of bool the carrier of R
{b} is non empty trivial 1 -element Element of bool the carrier of R
(R,{b}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {b} or not (R,b1,b2) )
}
is set

(R,{b}) /\ R is Element of bool the carrier of R
f is Element of the carrier of R
(R,R,f) is Element of bool the carrier of R
{f} is non empty trivial 1 -element Element of bool the carrier of R
(R,{f}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {f} or not (R,b1,b2) )
}
is set

(R,{f}) /\ R is Element of bool the carrier of R
(R,R,f) is Element of bool the carrier of R
(R,{f}) /\ R is Element of bool the carrier of R
f is set
e is Element of the carrier of R
(R,R,b) is Element of bool the carrier of R
{b} is non empty trivial 1 -element Element of bool the carrier of R
(R,{b}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {b} or not (R,b1,b2) )
}
is set

(R,{b}) /\ R is Element of bool the carrier of R
f is Element of the carrier of R
(R,R,f) is Element of bool the carrier of R
{f} is non empty trivial 1 -element Element of bool the carrier of R
(R,{f}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {f} or not (R,b1,b2) )
}
is set

(R,{f}) /\ R is Element of bool the carrier of R
(R,R,f) is Element of bool the carrier of R
(R,{f}) /\ R is Element of bool the carrier of R
(R,R,b) is Element of bool the carrier of R
{b} is non empty trivial 1 -element Element of bool the carrier of R
(R,{b}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {b} or not (R,b1,b2) )
}
is set

(R,{b}) /\ R is Element of bool the carrier of R
f is Element of the carrier of R
(R,R,f) is Element of bool the carrier of R
{f} is non empty trivial 1 -element Element of bool the carrier of R
(R,{f}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {f} or not (R,b1,b2) )
}
is set

(R,{f}) /\ R is Element of bool the carrier of R
(R,R,f) is Element of bool the carrier of R
(R,{f}) /\ R is Element of bool the carrier of R
b is Element of the carrier of R
d is Element of the carrier of R
(R,R,d) is Element of bool the carrier of R
{d} is non empty trivial 1 -element Element of bool the carrier of R
(R,{d}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {d} or not (R,b1,b2) )
}
is set

(R,{d}) /\ R is Element of bool the carrier of R
(R,R,d) is Element of bool the carrier of R
(R,{d}) /\ R is Element of bool the carrier of R
f is set
e is Element of the carrier of R
(R,R,b) is Element of bool the carrier of R
{b} is non empty trivial 1 -element Element of bool the carrier of R
(R,{b}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {b} or not (R,b1,b2) )
}
is set

(R,{b}) /\ R is Element of bool the carrier of R
f is Element of the carrier of R
(R,R,f) is Element of bool the carrier of R
{f} is non empty trivial 1 -element Element of bool the carrier of R
(R,{f}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {f} or not (R,b1,b2) )
}
is set

(R,{f}) /\ R is Element of bool the carrier of R
(R,R,f) is Element of bool the carrier of R
(R,{f}) /\ R is Element of bool the carrier of R
f is set
e is Element of the carrier of R
(R,R,b) is Element of bool the carrier of R
{b} is non empty trivial 1 -element Element of bool the carrier of R
(R,{b}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {b} or not (R,b1,b2) )
}
is set

(R,{b}) /\ R is Element of bool the carrier of R
f is Element of the carrier of R
(R,R,f) is Element of bool the carrier of R
{f} is non empty trivial 1 -element Element of bool the carrier of R
(R,{f}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {f} or not (R,b1,b2) )
}
is set

(R,{f}) /\ R is Element of bool the carrier of R
(R,R,f) is Element of bool the carrier of R
(R,{f}) /\ R is Element of bool the carrier of R
(R,R,b) is Element of bool the carrier of R
{b} is non empty trivial 1 -element Element of bool the carrier of R
(R,{b}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {b} or not (R,b1,b2) )
}
is set

(R,{b}) /\ R is Element of bool the carrier of R
f is Element of the carrier of R
(R,R,f) is Element of bool the carrier of R
{f} is non empty trivial 1 -element Element of bool the carrier of R
(R,{f}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {f} or not (R,b1,b2) )
}
is set

(R,{f}) /\ R is Element of bool the carrier of R
(R,R,f) is Element of bool the carrier of R
(R,{f}) /\ R is Element of bool the carrier of R
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
d is Element of the carrier of R
(R,R,d) is Element of bool the carrier of R
{d} is non empty trivial 1 -element Element of bool the carrier of R
(R,{d}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {d} or not (R,b1,b2) )
}
is set

(R,{d}) /\ R is Element of bool the carrier of R
b is Element of the carrier of R
(R,R,b) is Element of bool the carrier of R
{b} is non empty trivial 1 -element Element of bool the carrier of R
(R,{b}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {b} or not (R,b1,b2) )
}
is set

(R,{b}) /\ R is Element of bool the carrier of R
(R,(R,R,d)) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in (R,R,d) or not (R,b2,b1) )
}
is set

X . (R,(R,R,d)) is set
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
R is (R) (R,X)
R is (R) (R,X)
B is Element of the carrier of R
(R,R,B) is Element of bool the carrier of R
{B} is non empty trivial 1 -element Element of bool the carrier of R
(R,{B}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {B} or not (R,b1,b2) )
}
is set

(R,{B}) /\ R is Element of bool the carrier of R
B is Element of the carrier of R
(R,R,B) is Element of bool the carrier of R
{B} is non empty trivial 1 -element Element of bool the carrier of R
(R,{B}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {B} or not (R,b1,b2) )
}
is set

(R,{B}) /\ R is Element of bool the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
R is set
R is set
R is set
R is set
B is set
B is set
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
(R,X) is set
the (R) (R,X) is (R) (R,X)
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
(R,X) is non empty set
union (R,X) is set
R is set
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
(R,X) is non empty set
union (R,X) is set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
R is Element of bool the carrier of R
R is set
B is set
[R,B] is set
{R,B} is non empty set
{R} is non empty trivial 1 -element set
{{R,B},{R}} is non empty set
[B,R] is set
{B,R} is non empty set
{B} is non empty trivial 1 -element set
{{B,R},{B}} is non empty set
e is set
d is set
b is (R) (R,X)
f is (R) (R,X)
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
(R,X) is non empty set
union (R,X) is set
X . the carrier of R is set
{(X . the carrier of R)} is non empty trivial 1 -element set
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
BOOL the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Element of bool the carrier of R
R is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
(R,R) is non empty set
union (R,R) is set
R is (R) (R,R)
X \ R is Element of bool the carrier of R
the Element of X \ R is Element of X \ R
e is set
d is (R) (R,R)
b is Element of the carrier of R
(R,d,b) is Element of bool the carrier of R
{b} is non empty trivial 1 -element Element of bool the carrier of R
(R,{b}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {b} or not (R,b1,b2) )
}
is set

(R,{b}) /\ d is Element of bool the carrier of R
(R,X,b) is Element of bool the carrier of R
(R,{b}) /\ X is Element of bool the carrier of R
f is set
e is Element of the carrier of R
f is set
b is (R) (R,R)
b is (R) (R,R)
b is (R) (R,R)
f is set
R is non empty () () () () ()
the carrier of R is non empty set
BOOL the carrier of R is non empty set
bool the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
X is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
(R,X) is non empty set
union (R,X) is set
R is Element of the carrier of R
R is (R) Element of bool the carrier of R
B is set
(R,R,R) is Element of bool the carrier of R
{R} is non empty trivial 1 -element Element of bool the carrier of R
(R,{R}) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in {R} or not (R,b1,b2) )
}
is set

(R,{R}) /\ R is Element of bool the carrier of R
e is (R) (R,X)
(R,e,R) is Element of bool the carrier of R
(R,{R}) /\ e is Element of bool the carrier of R
(R,(R,R,R)) is Element of bool the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in (R,R,R) or not (R,b2,b1) )
}
is set

X . (R,(R,R,R)) is set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
R is set
the Element of R is Element of R
e is set
d is (R) (R,X)
d /\ R is Element of bool the carrier of R
b is set
the of R -Seg b is set
Coim ( the of R,b) is set
{b} is non empty trivial 1 -element set
the of R " {b} is set
(Coim ( the of R,b)) \ {b} is Element of bool (Coim ( the of R,b))
bool (Coim ( the of R,b)) is non empty set
( the of R -Seg b) /\ R is set
e is set
[e,b] is set
{e,b} is non empty set
{e} is non empty trivial 1 -element set
{{e,b},{e}} is non empty set
f is Element of the carrier of R
f is Element of the carrier of R
[b,e] is set
{b,e} is non empty set
{{b,e},{b}} is non empty set
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is Element of bool the carrier of R
the of R |_2 X is Relation-like set
[:X,X:] is set
the of R /\ [:X,X:] is set
field ( the of R |_2 X) is set
dom ( the of R |_2 X) is set
rng ( the of R |_2 X) is set
(dom ( the of R |_2 X)) \/ (rng ( the of R |_2 X)) is set
R is set
[R,R] is set
{R,R} is non empty set
{R} is non empty trivial 1 -element set
{{R,R},{R}} is non empty set
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is Element of bool the carrier of R
the of R |_2 X is Relation-like set
[:X,X:] is set
the of R /\ [:X,X:] is set
field ( the of R |_2 X) is set
dom ( the of R |_2 X) is set
rng ( the of R |_2 X) is set
(dom ( the of R |_2 X)) \/ (rng ( the of R |_2 X)) is set
R is set
R is set
[R,R] is set
{R,R} is non empty set
{R} is non empty trivial 1 -element set
{{R,R},{R}} is non empty set
[R,R] is set
{R,R} is non empty set
{R} is non empty trivial 1 -element set
{{R,R},{R}} is non empty set
B is Element of the carrier of R
e is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is (R) Element of bool the carrier of R
the of R |_2 X is Relation-like set
[:X,X:] is set
the of R /\ [:X,X:] is set
R is set
B is set
[R,B] is set
{R,B} is non empty set
{R} is non empty trivial 1 -element set
{{R,B},{R}} is non empty set
[B,R] is set
{B,R} is non empty set
{B} is non empty trivial 1 -element set
{{B,R},{B}} is non empty set
field ( the of R |_2 X) is set
dom ( the of R |_2 X) is set
rng ( the of R |_2 X) is set
(dom ( the of R |_2 X)) \/ (rng ( the of R |_2 X)) is set
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is Element of bool the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is (R) Element of bool the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is Element of the carrier of R
field the of R is set
dom the of R is set
rng the of R is set
(dom the of R) \/ (rng the of R) is set
R is Element of the carrier of R
[R,X] is Element of [: the carrier of R, the carrier of R:]
{R,X} is non empty set
{R} is non empty trivial 1 -element set
{{R,X},{R}} is non empty set
R is set
[R,X] is set
{R,X} is non empty set
{R} is non empty trivial 1 -element set
{{R,X},{R}} is non empty set
R is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is Element of the carrier of R
field the of R is set
dom the of R is set
rng the of R is set
(dom the of R) \/ (rng the of R) is set
R is Element of the carrier of R
[X,R] is Element of [: the carrier of R, the carrier of R:]
{X,R} is non empty set
{X} is non empty trivial 1 -element set
{{X,R},{X}} is non empty set
R is set
[X,R] is set
{X,R} is non empty set
{X} is non empty trivial 1 -element set
{{X,R},{X}} is non empty set
R is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is Element of the carrier of R
field the of R is set
dom the of R is set
rng the of R is set
(dom the of R) \/ (rng the of R) is set
R is Element of the carrier of R
[R,X] is Element of [: the carrier of R, the carrier of R:]
{R,X} is non empty set
{R} is non empty trivial 1 -element set
{{R,X},{R}} is non empty set
R is set
[R,X] is set
{R,X} is non empty set
{R} is non empty trivial 1 -element set
{{R,X},{R}} is non empty set
R is Element of the carrier of R
R is non empty () () () () ()
the carrier of R is non empty set
the of R is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive total Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty set
bool [: the carrier of R, the carrier of R:] is non empty set
X is Element of the carrier of R
field the of R is set
dom the of R is set
rng the of R is set
(dom the of R) \/ (rng the of R) is set
R is Element of the carrier of R
[X,R] is Element of [: the carrier of R, the carrier of R:]
{X,R} is non empty set
{X} is non empty trivial 1 -element set
{{X,R},{X}} is non empty set
R is set
[X,R] is set
{X,R} is non empty set
{X} is non empty trivial 1 -element set
{{X,R},{X}} is non empty set
R is Element of the carrier of R
R is set
X is set

R is set
B is set
[R,B] is set
{R,B} is non empty set
{R} is non empty trivial 1 -element set
{{R,B},{R}} is non empty set
[B,R] is set
{B,R} is non empty set
{B} is non empty trivial 1 -element set
{{B,R},{B}} is non empty set
R is set
X is set

R is set
R is non empty () () () () ()
the carrier of R is non empty set
bool the carrier of R is non empty set
BOOL the carrier of R is non empty set
K150( the carrier of R) is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
K150( the carrier of R) \ is Element of bool (bool the carrier of R)
union (BOOL the carrier of R) is set
the Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R is Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R
(R, the Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R) is non empty set
union (R, the Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R) is set
R is (R) (R, the Relation-like BOOL the carrier of R -defined union (BOOL the carrier of R) -valued Function-like V28( BOOL the carrier of R, union (BOOL the carrier of R)) Choice_Function of BOOL the carrier of R)
R is Element of the carrier of R
B is Element of the carrier of R
e is Element of the carrier of R
{ b1 where b1 is Element of the carrier of R : for b2 being Element of the carrier of R holds
( not b2 in R or not (R,b2,b1) )
}
is set

(