:: WAYBEL_8 semantic presentation

K129() is set

K133() is non empty non trivial V35() V36() V37() non finite cardinal limit_cardinal Element of bool K129()

bool K129() is non empty set

K128() is non empty non trivial V35() V36() V37() non finite cardinal limit_cardinal set

bool K128() is non empty non trivial non finite set

{} is empty V35() V36() V37() V39() V40() V41() finite V48() cardinal {} -element set

1 is non empty V35() V36() V37() V41() finite cardinal Element of K133()

{{},1} is non empty finite V48() set

bool K133() is non empty non trivial non finite set

K520() is set

{{}} is non empty trivial finite V48() 1 -element set

K498({{}}) is M34({{}})

[:K498({{}}),{{}}:] is set

bool [:K498({{}}),{{}}:] is non empty set

K98(K498({{}}),{{}}) is set

X is non empty reflexive RelStr

the carrier of X is non empty set

bool the carrier of X is non empty set

x is Element of bool the carrier of X

the InternalRel 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

the InternalRel of X |_2 x is Relation-like x -defined x -valued Element of bool [:x,x:]

[:x,x:] is set

bool [:x,x:] is non empty set

RelStr(# x,( the InternalRel of X |_2 x) #) is strict RelStr

a is strict reflexive full SubRelStr of X

the carrier of a is set

t is Element of the carrier of X

t1 is Element of the carrier of X

x is strict reflexive full SubRelStr of X

the carrier of x is set

a is strict reflexive full SubRelStr of X

the carrier of a is set

t is set

t1 is Element of the carrier of X

t1 is Element of the carrier of X

X is non empty reflexive antisymmetric lower-bounded RelStr

(X) is strict reflexive antisymmetric full SubRelStr of X

Bottom X is Element of the carrier of X

the carrier of X is non empty set

X is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr

the carrier of X is non empty set

(X) is non empty strict reflexive transitive antisymmetric full SubRelStr of X

the carrier of (X) is non empty set

x is Element of the carrier of X

t is Element of the carrier of X

a is Element of the carrier of X

X is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr

the carrier of X is non empty set

bool the carrier of X is non empty set

x is Element of the carrier of X

uparrow x is non empty filtered upper Element of bool the carrier of X

a is Element of the carrier of X

a is Element of the carrier of X

t is Element of the carrier of X

X is non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr

(X) is non empty strict reflexive transitive antisymmetric full SubRelStr of X

Bottom X is Element of the carrier of X

the carrier of X is non empty set

the carrier of (X) is non empty set

x is Element of the carrier of X

a is Element of the carrier of X

{x,a} is non empty finite Element of bool the carrier of X

bool the carrier of X is non empty set

x "\/" a is Element of the carrier of X

"\/" ({x,a},X) is Element of the carrier of X

X is non empty reflexive RelStr

the carrier of X is non empty set

x is Element of the carrier of X

{ b

bool the carrier of X is non empty set

t is Element of bool the carrier of X

t1 is set

Z is Element of the carrier of X

Z is Element of the carrier of X

X is non empty reflexive RelStr

the carrier of X is non empty set

a is Element of the carrier of X

x is Element of the carrier of X

(X,x) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

t is Element of the carrier of X

X is non empty reflexive RelStr

the carrier of X is non empty set

(X) is strict reflexive full SubRelStr of X

the carrier of (X) is set

x is Element of the carrier of X

(X,x) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

downarrow x is non empty directed Element of bool the carrier of X

(downarrow x) /\ the carrier of (X) is Element of bool the carrier of X

a is set

t is Element of the carrier of X

a is set

t is Element of the carrier of X

X is non empty reflexive transitive RelStr

the carrier of X is non empty set

x is Element of the carrier of X

(X,x) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

waybelow x is lower Element of bool the carrier of X

a is set

t is Element of the carrier of X

X is non empty reflexive antisymmetric lower-bounded RelStr

the carrier of X is non empty set

x is Element of the carrier of X

(X,x) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

Bottom X is Element of the carrier of X

X is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of X is non empty set

(X) is strict reflexive transitive antisymmetric full SubRelStr of X

the carrier of (X) is set

x is Element of the carrier of X

(X,x) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

waybelow x is directed lower Element of bool the carrier of X

a is set

"\/" ((X,x),X) is Element of the carrier of X

"\/" ((waybelow x),X) is Element of the carrier of X

x is Element of the carrier of X

waybelow x is directed lower Element of bool the carrier of X

(X,x) is Element of bool the carrier of X

{ b

x is Element of the carrier of X

a is Element of the carrier of X

(X,a) is Element of bool the carrier of X

{ b

t is non empty directed Element of bool the carrier of X

"\/" (t,X) is Element of the carrier of X

t1 is Element of the carrier of X

x is Element of the carrier of X

waybelow x is directed lower Element of bool the carrier of X

bool the carrier of X is non empty set

a is Element of the carrier of X

(X,x) is Element of bool the carrier of X

{ b

t is Element of the carrier of X

t is Element of the carrier of X

t1 is Element of the carrier of X

"\/" ((waybelow x),X) is Element of the carrier of X

"\/" ((X,x),X) is Element of the carrier of X

x is Element of the carrier of X

(X,x) is Element of bool the carrier of X

{ b

bool (X,x) is non empty set

waybelow x is directed lower Element of bool the carrier of X

a is finite Element of bool (X,x)

bool (waybelow x) is non empty set

t is Element of the carrier of X

t1 is Element of the carrier of X

Z is Element of the carrier of X

X is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

X is non empty reflexive RelStr

X is non empty reflexive transitive antisymmetric with_suprema RelStr

(X) is strict reflexive transitive antisymmetric full SubRelStr of X

the carrier of X is non empty set

x is Element of the carrier of X

the carrier of (X) is set

a is Element of the carrier of X

{x,a} is non empty finite Element of bool the carrier of X

bool the carrier of X is non empty set

x "\/" a is Element of the carrier of X

"\/" ({x,a},X) is Element of the carrier of X

X is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

X is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

x is non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() connected up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous RelStr

the carrier of x is non empty trivial finite 1 -element set

(x) is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of x

the carrier of (x) is non empty set

a is Element of the carrier of x

t is Element of the carrier of x

t1 is Element of the carrier of x

a is Element of the carrier of x

t is Element of the carrier of x

{a,t} is non empty trivial finite 1 -element directed filtered Element of bool the carrier of x

bool the carrier of x is non empty finite V48() set

"/\" ({a,t},x) is Element of the carrier of x

the non empty trivial finite 1 -element strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() connected up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous () () () RelStr is non empty trivial finite 1 -element strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() connected up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous () () () RelStr

X is non empty reflexive antisymmetric RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

x is non empty reflexive antisymmetric RelStr

the carrier of x is non empty set

the InternalRel 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

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

a is Element of the carrier of X

t is Element of the carrier of X

t1 is Element of the carrier of x

Z is Element of the carrier of x

bool the carrier of x is non empty set

bool the carrier of X is non empty set

k is non empty directed Element of bool the carrier of x

z is Element of bool the carrier of X

z2 is non empty directed Element of bool the carrier of X

"\/" (z2,X) is Element of the carrier of X

"\/" (k,x) is Element of the carrier of x

d is Element of the carrier of X

e is Element of the carrier of x

e is Element of the carrier of x

X is non empty reflexive antisymmetric RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

x is non empty reflexive antisymmetric RelStr

the carrier of x is non empty set

the InternalRel 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

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

a is Element of the carrier of X

t is Element of the carrier of x

X is non empty reflexive antisymmetric up-complete RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

x is non empty reflexive antisymmetric up-complete RelStr

the carrier of x is non empty set

the InternalRel 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

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

a is Element of the carrier of X

(X,a) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

t is Element of the carrier of x

(x,t) is Element of bool the carrier of x

bool the carrier of x is non empty set

{ b

t1 is set

Z is Element of the carrier of x

k is Element of the carrier of X

t1 is set

Z is Element of the carrier of X

k is Element of the carrier of x

X is RelStr

the carrier of X is set

the InternalRel 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 set

bool [: the carrier of X, the carrier of X:] is non empty set

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

x is RelStr

the carrier of x is set

the InternalRel 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 set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

X is RelStr

the carrier of X is set

the InternalRel 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 set

bool [: the carrier of X, the carrier of X:] is non empty set

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

x is RelStr

the carrier of x is set

the InternalRel 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 set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

a is set

[a,a] is set

{a,a} is non empty finite set

{a} is non empty trivial finite 1 -element set

{{a,a},{a}} is non empty finite V48() set

X is RelStr

the carrier of X is set

the InternalRel 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 set

bool [: the carrier of X, the carrier of X:] is non empty set

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

x is RelStr

the carrier of x is set

the InternalRel 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 set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

a is Element of the carrier of x

t is Element of the carrier of x

t1 is Element of the carrier of x

Z is Element of the carrier of X

k is Element of the carrier of X

z is Element of the carrier of X

X is RelStr

the carrier of X is set

the InternalRel 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 set

bool [: the carrier of X, the carrier of X:] is non empty set

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

x is RelStr

the carrier of x is set

the InternalRel 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 set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

a is Element of the carrier of x

t is Element of the carrier of x

t1 is Element of the carrier of X

Z is Element of the carrier of X

X is non empty reflexive RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

x is non empty reflexive RelStr

the carrier of x is non empty set

the InternalRel 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

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

bool the carrier of x is non empty set

bool the carrier of X is non empty set

a is non empty directed Element of bool the carrier of x

t is Element of bool the carrier of X

t1 is non empty directed Element of bool the carrier of X

Z is Element of the carrier of X

k is Element of the carrier of x

z is Element of the carrier of x

z2 is Element of the carrier of x

d is Element of the carrier of X

X is non empty reflexive antisymmetric up-complete RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

x is non empty reflexive antisymmetric up-complete RelStr

the carrier of x is non empty set

the InternalRel 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

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

a is Element of the carrier of x

t is Element of the carrier of X

(X,t) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

"\/" ((X,t),X) is Element of the carrier of X

(x,a) is Element of bool the carrier of x

bool the carrier of x is non empty set

{ b

"\/" ((x,a),x) is Element of the carrier of x

X is non empty reflexive antisymmetric RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

x is non empty reflexive antisymmetric RelStr

the carrier of x is non empty set

the InternalRel 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

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

a is Element of the carrier of x

(x,a) is Element of bool the carrier of x

bool the carrier of x is non empty set

{ b

t is Element of the carrier of X

(X,t) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

a is Element of the carrier of X

(X,a) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

t is Element of the carrier of X

(X,t) is Element of bool the carrier of X

{ b

X is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

x is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of x is non empty set

the InternalRel 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

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

(X) is strict reflexive transitive antisymmetric full join-inheriting SubRelStr of X

a is Element of the carrier of x

t is Element of the carrier of x

(x) is strict reflexive transitive antisymmetric full join-inheriting SubRelStr of x

the carrier of (x) is set

{a,t} is non empty finite Element of bool the carrier of x

bool the carrier of x is non empty set

t1 is Element of the carrier of X

the carrier of (X) is set

Z is Element of the carrier of X

{t1,Z} is non empty finite Element of bool the carrier of X

bool the carrier of X is non empty set

"/\" ({t1,Z},X) is Element of the carrier of X

"/\" ({a,t},x) is Element of the carrier of x

X is non empty RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

X is non empty reflexive RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is non empty strict RelStr

X is transitive RelStr

the carrier of X is set

the InternalRel 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 set

bool [: the carrier of X, the carrier of X:] is non empty set

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

X is antisymmetric RelStr

the carrier of X is set

the InternalRel 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 set

bool [: the carrier of X, the carrier of X:] is non empty set

RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr

X is non empty with_infima RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is non empty strict RelStr

X is non empty with_suprema RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is non empty strict RelStr

X is non empty reflexive up-complete RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is non empty strict reflexive RelStr

X is non empty reflexive antisymmetric up-complete () () RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is non empty strict reflexive antisymmetric up-complete RelStr

X is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous () () () RelStr

the carrier of X is non empty set

the InternalRel 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

RelStr(# the carrier of X, the InternalRel of X #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous () () RelStr

X is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous () () RelStr

(X) is strict reflexive transitive antisymmetric full join-inheriting SubRelStr of X

the carrier of X is non empty set

the Element of the carrier of X is Element of the carrier of X

(X, the Element of the carrier of X) is Element of bool the carrier of X

bool the carrier of X is non empty set

{ b

a is set

t is Element of the carrier of X

the carrier of X is non empty set

x is Element of the carrier of X

the carrier of (X) is set

a is Element of the carrier of X

{x,a} is non empty finite Element of bool the carrier of X

bool the carrier of X is non empty set

t is non empty reflexive transitive antisymmetric full SubRelStr of X

the carrier of t is non empty set

"/\" ({x,a},X) is Element of the carrier of X

(X,("/\" ({x,a},X))) is Element of bool the carrier of X

{ b

"/\" ({x,a},t) is Element of the carrier of t

"\/" ((X,("/\" ({x,a},X))),X) is Element of the carrier of X

t1 is Element of the carrier of t

Z is Element of the carrier of t

{t1,Z} is non empty finite Element of bool the carrier of t

bool the carrier of t is non empty set

z2 is set

d is Element of the carrier of X

x "/\" a is Element of the carrier of X

(X,a) is Element of bool the carrier of X

{ b

(X,x) is Element of bool the carrier of X

{ b

(X,x) /\ (X,a) is Element of bool the carrier of X

z2 is Element of the carrier of t

d is Element of the carrier of X

t1 "/\" Z is Element of the carrier of t

z2 is set

d is Element of the carrier of X

z is Element of the carrier of X

X is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous () () RelStr

X -waybelow is Relation-like the carrier of X -defined the carrier of X -valued transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT Element of bool [: the carrier of X, the carrier of X:]

the carrier of X is non empty set

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

(X) is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of X

a is Element of the carrier of X

t is Element of the carrier of X

[a,t] is Element of [: the carrier of X, the carrier of X:]

{a,t} is non empty finite set

{a} is non empty trivial finite 1 -element set

{{a,t},{a}} is non empty finite V48() set

t1 is Element of the carrier of X

[a,t1] is Element of [: the carrier of X, the carrier of X:]

{a,t1} is non empty finite set

{{a,t1},{a}} is non empty finite V48() set

the carrier of (X) is non empty set

Z is Element of the carrier of X

k is Element of the carrier of X

Z "/\" k is Element of the carrier of X

t "/\" t1 is Element of the carrier of X

x is non empty reflexive transitive antisymmetric with_infima full meet-inheriting SubRelStr of X

the carrier of x is non empty set

z is Element of the carrier of x

z2 is Element of the carrier of x

z "/\" z2 is Element of the carrier of x

a "/\" a is Element of the carrier of X

[a,(t "/\" t1)] is Element of [: the carrier of X, the carrier of X:]

{a,(t "/\" t1)} is non empty finite set

{{a,(t "/\" t1)},{a}} is non empty finite V48() set

x is Element of the carrier of X

(X) is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of X

the carrier of (X) is non empty set

a is Element of the carrier of X

{x,a} is non empty finite Element of bool the carrier of X

bool the carrier of X is non empty set

[a,a] is Element of [: the carrier of X, the carrier of X:]

{a,a} is non empty finite set

{a} is non empty trivial finite 1 -element set

{{a,a},{a}} is non empty finite V48() set

[x,x] is Element of [: the carrier of X, the carrier of X:]

{x,x} is non empty finite set

{x} is non empty trivial finite 1 -element set

{{x,x},{x}} is non empty finite V48() set

x "/\" a is Element of the carrier of X

[(x "/\" a),(x "/\" a)] is Element of [: the carrier of X, the carrier of X:]

{(x "/\" a),(x "/\" a)} is non empty finite set

{(x "/\" a)} is non empty trivial finite 1 -element set

{{(x "/\" a),(x "/\" a)},{(x "/\" a)}} is non empty finite V48() set

"/\" ({x,a},X) is Element of the carrier of X

X is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous () () () RelStr

the carrier of X is non empty set

x is Element of the carrier of X

X -waybelow is Relation-like the carrier of X -defined the carrier of X -valued transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT 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

X is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive satisfying_axiom_of_approximation continuous () () RelStr

the carrier of X is non empty set

X -waybelow is Relation-like the carrier of X -defined the carrier of X -valued transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT 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

X is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous () () RelStr

the carrier of X is non empty set

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

x is Relation-like the carrier of X -defined the carrier of X -valued Function-like V32( the carrier of X, the carrier of X) projection closure Element of bool [: the carrier of X, the carrier of X:]

Image x is non empty strict reflexive transitive antisymmetric full SubRelStr of X

rng x is Element of bool the carrier of X

bool the carrier of X is non empty set

subrelstr (rng x) is strict reflexive transitive antisymmetric full SubRelStr of X

the carrier of (Image x) is non empty set

bool the carrier of (Image x) is non empty set

the Element of the carrier of (Image x) is Element of the carrier of (Image x)

downarrow the Element of the carrier of (Image x) is non empty directed lower Element of bool the carrier of (Image x)

X is non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous () () RelStr

the carrier of X is non empty set

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

(X) is strict reflexive transitive antisymmetric full join-inheriting SubRelStr of X

[#] (X) is non proper Element of bool the carrier of (X)

the carrier of (X) is set

bool the carrier of (X) is non empty set

x is Relation-like the carrier of X -defined the carrier of X -valued Function-like V32( the carrier of X, the carrier of X) projection closure Element of bool [: the carrier of X, the carrier of X:]

x .: ([#] (X)) is Element of bool the carrier of X

bool the carrier of X is non empty set

Image x is non empty strict reflexive transitive antisymmetric full SubRelStr of X

rng x is Element of bool the carrier of X

subrelstr (rng x) is strict reflexive transitive antisymmetric full SubRelStr of X

((Image x)) is strict reflexive transitive antisymmetric full SubRelStr of Image x

[#] ((Image x)) is non proper Element of bool the carrier of ((Image x))

the carrier of ((Image x)) is set

bool the carrier of ((Image x)) is non empty set

a is set

dom x is Element of bool the carrier of X

t is set

x . t is set

the carrier of (Image x) is non empty set

t1 is Element of the carrier of (Image x)

k is Element of the carrier of X

id X is Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one V32( the carrier of X, the carrier of X) monotone isomorphic projection closure kernel Element of bool [: the carrier of X, the carrier of X:]

K100( the carrier of X) is non empty Relation-like the carrier of X -defined the carrier of X -valued V27( the carrier of X) Element of bool [: the carrier of X, the carrier of X:]

(id X) . k is Element of the carrier of X

x . k is Element of the carrier of X

Z is Element of the carrier of X

bool the carrier of (Image x) is non empty set

z is non empty directed Element of bool the carrier of (Image x)

"\/" (z,(Image x)) is Element of the carrier of (Image x)

z2 is non empty Element of bool the carrier of X

d is non empty directed Element of bool the carrier of X

"\/" (d,X) is Element of the carrier of X

x . ("\/" (d,X)) is Element of the carrier of X

x .: d is non empty Element of bool the carrier of X

"\/" ((x .: d),X) is Element of the carrier of X

e is Element of the carrier of X

e is Element of the carrier of (Image x)

d is Element of the carrier of (Image x)

{ b

x . e is Element of the carrier of X

z is Element of the carrier of X

x . z is Element of the carrier of X

X is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous () () RelStr

the carrier of X is non empty set

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

x is Relation-like the carrier of X -defined the carrier of X -valued Function-like V32( the carrier of X, the carrier of X) projection closure Element of bool [: the carrier of X, the carrier of X:]

Image x is non empty strict reflexive transitive antisymmetric full SubRelStr of X

rng x is Element of bool the carrier of X

bool the carrier of X is non empty set

subrelstr (rng x) is strict reflexive transitive antisymmetric full SubRelStr of X

a is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr

the carrier of a is non empty set

t1 is Element of the carrier of a

t is Element of the carrier of a

(a,t) is non empty Element of bool the carrier of a

bool the carrier of a is non empty set

{ b

Z is Element of the carrier of a

t1 "\/" Z is Element of the carrier of a

k is Element of the carrier of a

t is Element of the carrier of a

t1 is Element of the carrier of X

x . t1 is Element of the carrier of X

(X,t1) is non empty Element of bool the carrier of X

{ b

"\/" ((X,t1),X) is Element of the carrier of X

dom x is Element of bool the carrier of X

x . ("\/" ((X,t1),X)) is Element of the carrier of X

x .: (X,t1) is non empty Element of bool the carrier of X

"\/" ((x .: (X,t1)),X) is Element of the carrier of X

the carrier of (Image x) is non empty set

(a,t) is non empty Element of bool the carrier of a

{ b

Z is Element of the carrier of a

"\/" ((a,t),a) is Element of the carrier of a

(X) is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of X

[#] (X) is non empty non proper directed lower upper Element of bool the carrier of (X)

the carrier of (X) is non empty set

bool the carrier of (X) is non empty set

x .: ([#] (X)) is Element of bool the carrier of X

((Image x)) is strict reflexive transitive antisymmetric full SubRelStr of Image x

[#] ((Image x)) is non proper Element of bool the carrier of ((Image x))

the carrier of ((Image x)) is set

bool the carrier of ((Image x)) is non empty set

downarrow t1 is non empty directed lower Element of bool the carrier of X

(downarrow t1) /\ ([#] (X)) is Element of bool the carrier of (X)

x .: (downarrow t1) is non empty Element of bool the carrier of X

(x .: (downarrow t1)) /\ (x .: ([#] (X))) is Element of bool the carrier of X

Z is set

k is set

x . k is set

z2 is Element of the carrier of X

x . z2 is Element of the carrier of X

z is Element of the carrier of a

"\/" ((x .: (X,t1)),a) is Element of the carrier of a

X is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous () () RelStr

the carrier of X is non empty set

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

(X) is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of X

[#] (X) is non empty non proper directed lower upper Element of bool the carrier of (X)

the carrier of (X) is non empty set

bool the carrier of (X) is non empty set

x is Relation-like the carrier of X -defined the carrier of X -valued Function-like V32( the carrier of X, the carrier of X) projection closure Element of bool [: the carrier of X, the carrier of X:]

x .: ([#] (X)) is Element of bool the carrier of X

bool the carrier of X is non empty set

Image x is non empty strict reflexive transitive antisymmetric full SubRelStr of X

rng x is Element of bool the carrier of X

subrelstr (rng x) is strict reflexive transitive antisymmetric full SubRelStr of X

((Image x)) is strict reflexive transitive antisymmetric full SubRelStr of Image x

[#] ((Image x)) is non proper Element of bool the carrier of ((Image x))

the carrier of ((Image x)) is set

bool the carrier of ((Image x)) is non empty set

{ b

t is set

a is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr

(a) is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of a

the carrier of (a) is non empty set

the carrier of a is non empty set

t1 is Element of the carrier of a

Z is Element of the carrier of X

x . Z is Element of the carrier of X

(X,Z) is non empty Element of bool the carrier of X

{ b

k is set

x .: (X,Z) is non empty Element of bool the carrier of X

dom x is Element of bool the carrier of X

z is set

x . z is set

downarrow Z is non empty directed lower Element of bool the carrier of X

(downarrow Z) /\ the carrier of (X) is Element of bool the carrier of X

z2 is Element of the carrier of X

x . z2 is Element of the carrier of X

(downarrow Z) /\ (x .: ([#] (X))) is Element of bool the carrier of X

"\/" ((X,Z),X) is Element of the carrier of X

"\/" ((x .: (X,Z)),X) is Element of the carrier of X

downarrow t1 is non empty directed lower Element of bool the carrier of a

bool the carrier of a is non empty set

(downarrow t1) /\ (x .: ([#] (X))) is Element of bool the carrier of X

(x .: ([#] (X))) /\ (downarrow t1) is Element of bool the carrier of a

Bottom a is Element of the carrier of a

z is Element of the carrier of a

k is Element of bool the carrier of a

z2 is Element of the carrier of a

d is set

x . d is set

e is set

x . e is set

e is Element of the carrier of X

x . e is Element of the carrier of X

d is Element of the carrier of X

d "\/" e is Element of the carrier of X

x . d is Element of the carrier of X

(x . d) "\/" (x . e) is Element of the carrier of X

x . (d "\/" e) is Element of the carrier of X

z is Element of the carrier of a

id X is Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one V32( the carrier of X, the carrier of X) monotone isomorphic projection closure kernel Element of bool [: the carrier of X, the carrier of X:]

K100( the carrier of X) is non empty Relation-like the carrier of X -defined the carrier of X -valued V27( the carrier of X) Element of bool [: the carrier of X, the carrier of X:]

(id X) . e is Element of the carrier of X

(id X) . d is Element of the carrier of X

z is Element of the carrier of a

Bottom X is Element of the carrier of X

x . (Bottom X) is Element of the carrier of X

"\/" ({},X) is Element of the carrier of X

x . ("\/" ({},X)) is Element of the carrier of X

"\/" ({},a) is Element of the carrier of a

k is set

z is Element of the carrier of X

z2 is Element of the carrier of a

"\/" ((x .: (X,Z)),a) is Element of the carrier of a

"\/" (((downarrow t1) /\ (x .: ([#] (X)))),a) is Element of the carrier of a

k is Element of the carrier of a

x is set

X is set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean RelStr

the carrier of (BoolePoset X) is non empty set

BooleLatt X is non empty V120() V127() V134() complete L15()

LattPOSet (BooleLatt X) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr

the carrier of (BooleLatt X) is non empty set

LattRel (BooleLatt X) is Relation-like the carrier of (BooleLatt X) -defined the carrier of (BooleLatt X) -valued reflexive antisymmetric transitive V27( the carrier of (BooleLatt X)) Element of bool [: the carrier of (BooleLatt X), the carrier of (BooleLatt X):]

[: the carrier of (BooleLatt X), the carrier of (BooleLatt X):] is non empty set

bool [: the carrier of (BooleLatt X), the carrier of (BooleLatt X):] is non empty set

RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) is strict RelStr

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

X is set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean RelStr

the carrier of (BoolePoset X) is non empty set

bool X is non empty set

bool (bool X) is non empty set

x is Element of the carrier of (BoolePoset X)

a is Element of the carrier of (BoolePoset X)

BooleLatt X is non empty V120() V127() V134() complete L15()

LattPOSet (BooleLatt X) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete RelStr

the carrier of (BooleLatt X) is non empty set

LattRel (BooleLatt X) is Relation-like the carrier of (BooleLatt X) -defined the carrier of (BooleLatt X) -valued reflexive antisymmetric transitive V27( the carrier of (BooleLatt X)) Element of bool [: the carrier of (BooleLatt X), the carrier of (BooleLatt X):]

[: the carrier of (BooleLatt X), the carrier of (BooleLatt X):] is non empty set

bool [: the carrier of (BooleLatt X), the carrier of (BooleLatt X):] is non empty set

RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #) is strict RelStr

bool X is non empty Element of bool (bool X)

t is Element of bool (bool X)

union t is Element of bool X

bool t is non empty set

bool the carrier of (BoolePoset X) is non empty set

t1 is Element of bool the carrier of (BoolePoset X)

"\/" (t1,(BoolePoset X)) is Element of the carrier of (BoolePoset X)

Z is finite Element of bool the carrier of (BoolePoset X)

"\/" (Z,(BoolePoset X)) is Element of the carrier of (BoolePoset X)

k is finite Element of bool t

union k is set

bool the carrier of (BoolePoset X) is non empty set

t is Element of bool the carrier of (BoolePoset X)

"\/" (t,(BoolePoset X)) is Element of the carrier of (BoolePoset X)

t1 is Element of bool (bool X)

union t1 is Element of bool X

bool t1 is non empty set

Z is finite Element of bool t1

union Z is set

k is finite Element of bool the carrier of (BoolePoset X)

z is finite Element of bool the carrier of (BoolePoset X)

"\/" (z,(BoolePoset X)) is Element of the carrier of (BoolePoset X)

X is set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean RelStr

the carrier of (BoolePoset X) is non empty set

x is Element of the carrier of (BoolePoset X)

Bottom (BoolePoset X) is Element of the carrier of (BoolePoset X)

bool X is non empty set

bool (bool X) is non empty set

a is Element of bool (bool X)

union a is Element of bool X

t is set

t1 is set

t is Relation-like Function-like set

dom t is set

rng t is set

bool a is non empty set

t1 is Element of bool a

Z is finite Element of bool a

z is set

t . z is set

k is finite Element of bool a

union k is set

a is non empty set

{ {b

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

t1 is set

Z is set

k is Element of a

{k} is non empty trivial finite 1 -element Element of bool a

bool a is non empty set

Z is set

{Z} is non empty trivial finite 1 -element set

t1 is Element of bool (bool X)

union t1 is Element of bool X

bool t1 is non empty set

Z is finite Element of bool t1

union Z is set

k is set

z is Element of a

{z} is non empty trivial finite 1 -element Element of bool a

bool a is non empty set

X is set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean RelStr

the carrier of (BoolePoset X) is non empty set

x is Element of the carrier of (BoolePoset X)

((BoolePoset X),x) is non empty Element of bool the carrier of (BoolePoset X)

bool the carrier of (BoolePoset X) is non empty set

{ b

bool x is non empty set

{ b

a is set

t is finite Element of bool x

t1 is Element of the carrier of (BoolePoset X)

a is set

t is Element of the carrier of (BoolePoset X)

X is set

bool X is non empty set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean RelStr

((BoolePoset X)) is non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting SubRelStr of BoolePoset X

the carrier of ((BoolePoset X)) is non empty set

x is Element of bool X

the carrier of (BoolePoset X) is non empty set

t is Element of the carrier of (BoolePoset X)

((BoolePoset X),t) is non empty Element of bool the carrier of (BoolePoset X)

bool the carrier of (BoolePoset X) is non empty set

{ b

bool t is non empty set

{ b

t1 is finite Element of bool t

a is Element of the carrier of (BoolePoset X)

bool a is non empty set

{ b

((BoolePoset X),a) is non empty Element of bool the carrier of (BoolePoset X)

bool the carrier of (BoolePoset X) is non empty set

{ b

X is set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean RelStr

the carrier of (BoolePoset X) is non empty set

x is Element of the carrier of (BoolePoset X)

((BoolePoset X),x) is non empty Element of bool the carrier of (BoolePoset X)

bool the carrier of (BoolePoset X) is non empty set

{ b

a is set

t is set

bool x is non empty set

{ b

t1 is finite Element of bool x

a is set

t is set

a \/ t is set

t1 is finite Element of bool x

Z is finite Element of bool x

X is set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean RelStr

the carrier of (BoolePoset X) is non empty set

x is Element of the carrier of (BoolePoset X)

((BoolePoset X),x) is non empty directed lower Element of bool the carrier of (BoolePoset X)

bool the carrier of (BoolePoset X) is non empty set

{ b

a is Element of the carrier of (BoolePoset X)

t is set

t1 is set

{t} is non empty trivial finite 1 -element set

Z is set

bool x is non empty set

{ b

t1 is Element of the carrier of (BoolePoset X)

a is Element of the carrier of (BoolePoset X)

"\/" (((BoolePoset X),x),(BoolePoset X)) is Element of the carrier of (BoolePoset X)

x is Element of the carrier of (BoolePoset X)

((BoolePoset X),x) is non empty directed lower Element of bool the carrier of (BoolePoset X)

{ b

a is Element of the carrier of (BoolePoset X)

((BoolePoset X),a) is non empty directed lower Element of bool the carrier of (BoolePoset X)

{ b

X is set

BoolePoset X is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean RelStr