:: 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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(R,{e}) /\ B is Element of bool the carrier of R

(R,(R,B,e)) is Element of bool the carrier of R

{ b

( not b

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

( not b

(R,{e}) /\ B is Element of bool the carrier of R

(R,(R,B,e)) is Element of bool the carrier of R

{ b

( not b

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

( not b

(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

( not b

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

( not b

(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

( not b

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

( not b

(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

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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

(R,{b}) /\ R is Element of bool the carrier of R

(R,(R,R,d)) is Element of bool the carrier of R

{ b

( not b

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

( not b

(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

( not b

(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

( not b

(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

( not b

(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

( not b

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

( not b

(