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