:: 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
X is Relation-like R -defined R -valued Element of bool [:R,R:]
(R,X) is () ()
{{}} is non empty trivial 1 -element set
[:{{}},{{}}:] is non empty set
bool [:{{}},{{}}:] is non empty set
the Relation-like {{}} -defined {{}} -valued reflexive antisymmetric transitive total Element of bool [:{{}},{{}}:] is Relation-like {{}} -defined {{}} -valued reflexive antisymmetric transitive total Element of bool [:{{}},{{}}:]
({{}}, the Relation-like {{}} -defined {{}} -valued reflexive antisymmetric transitive total Element of bool [:{{}},{{}}:]) is non empty () ()
X is non empty () ()
field the Relation-like {{}} -defined {{}} -valued reflexive antisymmetric transitive total Element of bool [:{{}},{{}}:] is set
dom the Relation-like {{}} -defined {{}} -valued reflexive antisymmetric transitive total Element of bool [:{{}},{{}}:] is set
rng the Relation-like {{}} -defined {{}} -valued reflexive antisymmetric transitive total Element of bool [:{{}},{{}}:] is set
(dom the Relation-like {{}} -defined {{}} -valued reflexive antisymmetric transitive total Element of bool [:{{}},{{}}:]) \/ (rng the Relation-like {{}} -defined {{}} -valued reflexive antisymmetric transitive total Element of bool [:{{}},{{}}:]) 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
X is Relation-like R -defined R -valued reflexive total Element of bool [:R,R:]
(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
X is Relation-like R -defined R -valued transitive total Element of bool [:R,R:]
(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
X is Relation-like R -defined R -valued antisymmetric total Element of bool [:R,R:]
(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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in X or not (R,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in X or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {} R or not (R,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in [#] R or not (R,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {} R or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in [#] R or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in R or not (R,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {X} or not (R,b₂,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 the carrier of R
R is Element of bool the carrier of R
(R,R) is Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in R or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {X} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {X} or not (R,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {R} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {R} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {R} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {R} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {R} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {X} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {X} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {X} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {R} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {X} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {R} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {R} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {R} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {B} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {e} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {X} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {e} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {e} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {e} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in (R,B,e) or not (R,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {e} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in (R,B,e) or not (R,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {B} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in (R,{B}) /\ R or not (R,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {d} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in (R,{d}) /\ B or not (R,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {X} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : ( b₁ in R /\ R & (R,R,b₁) = (R,R,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {d} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {d} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {f} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {f} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {f} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {d} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {f} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {f} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {f} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {d} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in (R,R,d) or not (R,b₂,b₁) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {B} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {B} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {R} or not (R,b₁,b₂) ) } 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in (R,R,R) or not (R,b₂,b₁) ) } 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 Relation-like 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 Relation-like 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in R or not (R,b₂,b₁) ) } is set
(R,R) is Element of bool the carrier of 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,R) is set
e is Element of the carrier of R
{e} is non empty trivial 1 -element Element of bool the carrier of R
R \/ {e} 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 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 bool the carrier of R
b is set
f is set
[b,f] is set
{b,f} is non empty set
{b} is non empty trivial 1 -element set
{{b,f},{b}} is non empty set
[f,b] is set
{f,b} is non empty set
{f} is non empty trivial 1 -element set
{{f,b},{f}} is non empty set
e is Element of the carrier of R
f is Element of the carrier of R
e is Element of the carrier of R
f is Element of the carrier of R
b is Element of the carrier of R
e is Element of the carrier of R
f is Element of the carrier of R
b is Element of the carrier of R
e is Element of the carrier of R
f is Element of the carrier of R
e is Element of the carrier of R
f is Element of the carrier of R
b is Element of the carrier of R
(R,d,e) is Element of bool the carrier of R
(R,{e}) is Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {e} or not (R,b₁,b₂) ) } is set
(R,{e}) /\ d is Element of bool the carrier of R
f is set
f is set
e is Element of the carrier of R
f 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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } is set
(R,{b}) /\ d is Element of bool the carrier of R
(R,(R,d,b)) is Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in (R,d,b) or not (R,b₂,b₁) ) } 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 . (R,(R,d,b)) is set
(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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } is set
(R,{b}) /\ d 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
f is set
e is Element of the carrier of R
e is Element of the carrier of R
(R,(R,d,b)) is Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in (R,d,b) or not (R,b₂,b₁) ) } 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 . (R,(R,d,b)) is set
(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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } is set
(R,{b}) /\ d is Element of bool the carrier of R
(R,(R,d,b)) is Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in (R,d,b) or not (R,b₂,b₁) ) } 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 . (R,(R,d,b)) is set
(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
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in {b} or not (R,b₁,b₂) ) } is set
(R,{b}) /\ d is Element of bool the carrier of R
(R,(R,d,b)) is Element of bool the carrier of R
{ b₁ where b₁ is Element of the carrier of R : for b₂ being Element of the carrier of R holds
( not b₂ in (R,d,b) or not (R,b₂,b₁) ) } 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 . (R,(R,d,b)) is set
b is set
f is Element of the carrier of R
the of R -Seg f is set
Coim ( the of R,f) is set
{f} is non empty trivial 1 -element set
the of R " {f} is set
(Coim ( the of R,f)) \ {f} is Element of bool (Coim ( the of R,f))
bool (Coim ( the of R,f)) is non empty set
e is set
b \ {e} is Element of bool b
bool b is non empty set
e 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
f is set
( the of R -Seg e) /\ (b \ {e}) is Element of bool b
the of R -Seg f is set
Coim ( the of R,f) is set
{f} is non empty trivial 1 -element set
the of R " {f} is set
(Coim ( the of R,f)) \ {f} is Element of bool (Coim ( the of R,f))
bool (Coim ( the of R,f)) is non empty set
[e,f] is set
{e,f} is non empty set
{e} is non empty trivial 1 -element set
{{e,f},{e}} is non empty set
b is Element of the carrier of R
f1 is Element of the carrier of R
( the of R -Seg f) /\ {e} is Element of bool the carrier of R
the Element of ( the of R -Seg f) /\ {e} is Element of ( the of R -Seg f) /\ {e}
(b \ {e}) \/ {e} is non empty set
( the of R -Seg f) /\ b is set
{} \/ {} is set
the of R -Seg f is set
Coim ( the of R,f) is set
{f} is non empty trivial 1 -element set
the of R " {f} is set
(Coim ( the of R,f)) \ {f} is Element of bool (Coim ( the of R,f))
bool (Coim ( the of R,f)) is non empty set
the of R -Seg f is set
Coim ( the of R,f) is set
{f} is non empty trivial 1 -element set
the of R " {f} is set
(Coim ( the of R,f)) \ {f} is Element of bool (Coim ( the of R,f))
bool (Coim ( the of R,f)) is non empty set
the of R -Seg f is set
Coim ( the of R,f) is set
{f} is non empty trivial 1 -element set
the of R " {f} is set
(Coim ( the of R,f)) \ {f} is Element of bool (Coim ( the of R,f))
bool (Coim ( the of R,f)) is non empty set
f is Element of the carrier of R
the of R -Seg f is set
Coim ( the of R,f) is set
{f} is non empty trivial 1 -element set
the of R " {f} is set
(Coim ( the of R,f)) \ {f} is Element of bool (Coim ( the of R,f))
bool (Coim ( the of R,f)) is non empty 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
b 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)
f 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
the of R ~ is Relation-like the carrier of R -defined the carrier of R -valued reflexive antisymmetric transitive Element of bool [: the carrier of R, the carrier of R:]
dom ( the of R ~) is Element of bool the carrier of R
dom the of R is Element of bool the carrier of R
R is Element of the carrier of R
B is Element of the carrier of R
[R,B] is Element of [: the carrier of R, the carrier of R:]
{R,B} is non empty set
{R} is non empty trivial 1 -element set
{{R,B},{R}} is non empty set
[B,R] is Element of [: the carrier of R, the carrier of R:]
{B,R} is non empty set
{B} is non empty trivial 1 -element set
{{B,R},{B}} is non empty set
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,R) is non empty () () () () () ()
the carrier of ( the carrier of R,R) is non empty set
bool the carrier of ( the carrier of R,R) is non empty set
e is (( the carrier of R,R)) Element of bool the carrier of ( the carrier of R,R)
d is Element of bool the carrier of R
b is set
f is set
[b,f] is set
{b,f} is non empty set
{b} is non empty trivial 1 -element set
{{b,f},{b}} is non empty set
[f,b] is set
{f,b} is non empty set
{f} is non empty trivial 1 -element set
{{f,b},{f}} is non empty set
e is Element of the carrier of ( the carrier of R,R)
f is Element of the carrier of ( the carrier of R,R)
[e,f] is Element of [: the carrier of ( the carrier of R,R), the carrier of ( the carrier of R,R):]
[: the carrier of ( the carrier of R,R), the carrier of ( the carrier of R,R):] is non empty set
{e,f} is non empty set
{e} is non empty trivial 1 -element set
{{e,f},{e}} is non empty set
f1 is Element of the carrier of R
b is Element of the carrier of R
[f,e] is Element of [: the carrier of ( the carrier of R,R), the carrier of ( the carrier of R,R):]
[: the carrier of ( the carrier of R,R), the carrier of ( the carrier of R,R):] is non empty set
{f,e} is non empty set
{f} is non empty trivial 1 -element set
{{f,e},{f}} is non empty set
b is Element of the carrier of R
f1 is Element of the carrier of R
[e,f] is Element of [: the carrier of ( the carrier of R,R), the carrier of ( the carrier of R,R):]
[: the carrier of ( the carrier of R,R), the carrier of ( the carrier of R,R):] is non empty set
{e,f} is non empty set
{e} is non empty trivial 1 -element set
{{e,f},{e}} is non empty set
[f,e] is Element of [: the carrier of ( the carrier of R,R), the carrier of ( the carrier of R,R):]
{f,e} is non empty set
{f} is non empty trivial 1 -element set
{{f,e},{f}} is non empty set
b is (R) Element of bool the carrier of R
f is Element of the carrier of R
e is Element of the carrier of ( the carrier of R,R)
f is Element of the carrier of ( the carrier of R,R)
b is Element of the carrier of R
[f,e] is Element of [: the carrier of ( the carrier of R,R), the carrier of ( the carrier of R,R):]
[: the carrier of ( the carrier of R,R), the carrier of ( the carrier of R,R):] is non empty set
{f,e} is non empty set
{f} is non empty trivial 1 -element set
{{f,e},{f}} is non empty set
e is Element of the carrier of ( the carrier of R,R)
d is Element of the carrier of R
b is Element of the carrier of R
f is Element of the carrier of ( the carrier of R,R)
[e,f] is Element of [: the carrier of ( the carrier of R,R), the carrier of ( the carrier of R,R):]
[: the carrier of ( the carrier of R,R), the carrier of ( the carrier of R,R):] is non empty set
{e,f} is non empty set
{e} is non empty trivial 1 -element set
{{e,f},{e}} is non empty set
[:{},{}:] is set
bool [:{},{}:] is non empty set
the Relation-like {} -defined {} -valued reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive well-ordering empty total being_quasi-order being_partial-order being_linear-order V34() V35() V36() V38() V39() V40() V41() cardinal {} -element Element of bool [:{},{}:] is Relation-like {} -defined {} -valued reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive well-ordering empty total being_quasi-order being_partial-order being_linear-order V34() V35() V36() V38() V39() V40() V41() cardinal {} -element Element of bool [:{},{}:]
({}, the Relation-like {} -defined {} -valued reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive well-ordering empty total being_quasi-order being_partial-order being_linear-order V34() V35() V36() V38() V39() V40() V41() cardinal {} -element Element of bool [:{},{}:]) is () () () () () ()
R is () () () () () ()
the carrier of R is set