:: 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()
is set
bool 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

the carrier of a is set
t is Element of the carrier of X
t1 is Element of the carrier of X

the carrier of x is set

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

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

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 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
{ b1 where b1 is Element of the carrier of X : ( b1 <= x & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of X : ( b1 <= x & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of X : ( b1 <= x & b1 is compact ) } is set
downarrow x is non empty directed Element of bool the carrier of 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
{ b1 where b1 is Element of the carrier of X : ( b1 <= x & b1 is compact ) } is set
waybelow x is lower Element of bool the carrier of X
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
(X,x) is Element of bool the carrier of X
bool the carrier of X is non empty set
{ b1 where b1 is Element of the carrier of X : ( b1 <= x & b1 is compact ) } is set
Bottom X is Element of the carrier of X

the carrier of X is non empty set

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
{ b1 where b1 is Element of the carrier of X : ( b1 <= x & b1 is compact ) } is set
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
"\/" ((),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
{ b1 where b1 is Element of the carrier of X : ( b1 <= x & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of X : ( b1 <= a & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of X : ( b1 <= x & b1 is compact ) } is set
t is Element of the carrier of X
t is Element of the carrier of X
t1 is Element of the carrier of 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
{ b1 where b1 is Element of the carrier of X : ( b1 <= x & b1 is compact ) } is set
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 () 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 RelStr

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

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

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

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

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

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
{ b1 where b1 is Element of the carrier of X : ( b1 <= a & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of x : ( b1 <= t & b1 is compact ) } is set
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

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

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
{ b1 where b1 is Element of the carrier of X : ( b1 <= t & b1 is compact ) } is set
"\/" ((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
{ b1 where b1 is Element of the carrier of x : ( b1 <= a & b1 is compact ) } is set
"\/" ((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
{ b1 where b1 is Element of the carrier of x : ( b1 <= a & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of X : ( b1 <= t & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of X : ( b1 <= a & b1 is compact ) } is set
t is Element of the carrier of X
(X,t) is Element of bool the carrier of X
{ b1 where b1 is Element of the carrier of X : ( b1 <= t & b1 is compact ) } is set

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

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

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

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

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

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

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
{ b1 where b1 is Element of the carrier of X : ( b1 <= the Element of the carrier of X & b1 is compact ) } is set
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

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
{ b1 where b1 is Element of the carrier of X : ( b1 <= "/\" ({x,a},X) & b1 is compact ) } is set
"/\" ({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
{ b1 where b1 is Element of the carrier of X : ( b1 <= a & b1 is compact ) } is set
(X,x) is Element of bool the carrier of X
{ b1 where b1 is Element of the carrier of X : ( b1 <= x & b1 is compact ) } is set
(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

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

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

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

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

the carrier of X is non empty set
x is Element of 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 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

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

rng x is Element of bool the carrier of X
bool the carrier of X is non empty set

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

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

rng x is Element of bool the carrier of X

[#] (()) is non proper Element of bool the carrier of (())
the carrier of (()) is set
bool the carrier of (()) 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 () is non empty set
t1 is Element of the carrier of ()
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 () is non empty set
z is non empty directed Element of bool the carrier of ()
"\/" (z,()) is Element of the carrier of ()
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 ()
d is Element of the carrier of ()
{ b1 where b1 is Element of the carrier of X : b1 = x . b1 } is set
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

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

rng x is Element of bool the carrier of X
bool the carrier of X is non empty set

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
{ b1 where b1 is Element of the carrier of a : ( b1 <= t & b1 is compact ) } is set
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
{ b1 where b1 is Element of the carrier of X : ( b1 <= t1 & b1 is compact ) } is set
"\/" ((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 () is non empty set
(a,t) is non empty Element of bool the carrier of a
{ b1 where b1 is Element of the carrier of a : ( b1 <= t & b1 is compact ) } is set
Z is Element of the carrier of a
"\/" ((a,t),a) is Element of the carrier of a

[#] (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

[#] (()) is non proper Element of bool the carrier of (())
the carrier of (()) is set
bool the carrier of (()) is non empty set
downarrow t1 is non empty directed lower Element of bool the carrier of X
() /\ ([#] (X)) is Element of bool the carrier of (X)
x .: () is non empty Element of bool the carrier of X
(x .: ()) /\ (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

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

rng x is Element of bool the carrier of X

[#] (()) is non proper Element of bool the carrier of (())
the carrier of (()) is set
bool the carrier of (()) is non empty set
{ b1 where b1 is Element of the carrier of X : b1 = x . b1 } is set
t is set

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
{ b1 where b1 is Element of the carrier of X : ( b1 <= Z & b1 is compact ) } is set
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
() /\ 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
() /\ (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
() /\ (x .: ([#] (X))) is Element of bool the carrier of X
(x .: ([#] (X))) /\ () 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 . () 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
"\/" ((() /\ (x .: ([#] (X)))),a) is Element of the carrier of a
k is Element of the carrier of a
x is set
X is set

the carrier of () is non empty set
BooleLatt X is non empty V120() V127() V134() complete L15()

the carrier of () is non empty set
LattRel () is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V27( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),(LattRel ()) #) 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

the carrier of () is non empty set
bool X is non empty set
bool (bool X) is non empty set
x is Element of the carrier of ()
a is Element of the carrier of ()
BooleLatt X is non empty V120() V127() V134() complete L15()

the carrier of () is non empty set
LattRel () is Relation-like the carrier of () -defined the carrier of () -valued reflexive antisymmetric transitive V27( the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
RelStr(# the carrier of (),(LattRel ()) #) 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 () is non empty set
t1 is Element of bool the carrier of ()
"\/" (t1,()) is Element of the carrier of ()
Z is finite Element of bool the carrier of ()
"\/" (Z,()) is Element of the carrier of ()
k is finite Element of bool t
union k is set
bool the carrier of () is non empty set
t is Element of bool the carrier of ()
"\/" (t,()) is Element of the carrier of ()
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 ()
z is finite Element of bool the carrier of ()
"\/" (z,()) is Element of the carrier of ()
X is set

the carrier of () is non empty set
x is Element of the carrier of ()
Bottom () is Element of the carrier of ()
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

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
{ {b1} where b1 is Element of a : verum } is set
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

the carrier of () is non empty set
x is Element of the carrier of ()
((),x) is non empty Element of bool the carrier of ()
bool the carrier of () is non empty set
{ b1 where b1 is Element of the carrier of () : ( b1 <= x & b1 is compact ) } is set
bool x is non empty set
{ b1 where b1 is finite Element of bool x : verum } is set
a is set
t is finite Element of bool x
t1 is Element of the carrier of ()
a is set
t is Element of the carrier of ()
X is set
bool X is non empty set

the carrier of (()) is non empty set
x is Element of bool X
the carrier of () is non empty set
t is Element of the carrier of ()
((),t) is non empty Element of bool the carrier of ()
bool the carrier of () is non empty set
{ b1 where b1 is Element of the carrier of () : ( b1 <= t & b1 is compact ) } is set
bool t is non empty set
{ b1 where b1 is finite Element of bool t : verum } is set
t1 is finite Element of bool t
a is Element of the carrier of ()
bool a is non empty set
{ b1 where b1 is finite Element of bool a : verum } is set
((),a) is non empty Element of bool the carrier of ()
bool the carrier of () is non empty set
{ b1 where b1 is Element of the carrier of () : ( b1 <= a & b1 is compact ) } is set
X is set

the carrier of () is non empty set
x is Element of the carrier of ()
((),x) is non empty Element of bool the carrier of ()
bool the carrier of () is non empty set
{ b1 where b1 is Element of the carrier of () : ( b1 <= x & b1 is compact ) } is set
a is set
t is set
bool x is non empty set
{ b1 where b1 is finite Element of bool x : verum } is set
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

the carrier of () is non empty set
x is Element of the carrier of ()
((),x) is non empty directed lower Element of bool the carrier of ()
bool the carrier of () is non empty set
{ b1 where b1 is Element of the carrier of () : ( b1 <= x & b1 is compact ) } is set
a is Element of the carrier of ()
t is set
t1 is set
{t} is non empty trivial finite 1 -element set
Z is set
bool x is non empty set
{ b1 where b1 is finite Element of bool x : verum } is set
t1 is Element of the carrier of ()
a is Element of the carrier of ()
"\/" (((),x),()) is Element of the carrier of ()
x is Element of the carrier of ()
((),x) is non empty directed lower Element of bool the carrier of ()
{ b1 where b1 is Element of the carrier of () : ( b1 <= x & b1 is compact ) } is set
a is Element of the carrier of ()
((),a) is non empty directed lower Element of bool the carrier of ()
{ b1 where b1 is Element of the carrier of () : ( b1 <= a & b1 is compact ) } is set
X is set