:: WAYBEL_7 semantic presentation

K291() is Element of bool K287()
K287() is set
bool K287() is non empty set
omega is set
bool omega is non empty set
bool K291() is non empty set
{} is empty Relation-like non-empty empty-yielding finite finite-yielding V35() set
the empty Relation-like non-empty empty-yielding finite finite-yielding V35() set is empty Relation-like non-empty empty-yielding finite finite-yielding V35() set
1 is non empty set
union {} is finite set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr
a is set
x is set
"\/" (a,L) is Element of the carrier of L
the carrier of L is non empty set
"\/" (x,L) is Element of the carrier of L
"/\" (x,L) is Element of the carrier of L
"/\" (a,L) is Element of the carrier of L
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset L) is non empty set
bool L is non empty Element of bool (bool L)
bool L is non empty set
bool (bool L) is non empty set
InclPoset (bool L) is non empty strict reflexive transitive antisymmetric non void RelStr
RelIncl (bool L) is Relation-like V20( bool L) V75() V78() V82() Element of bool [:(bool L),(bool L):]
[:(bool L),(bool L):] is non empty Relation-like set
bool [:(bool L),(bool L):] is non empty set
RelStr(# (bool L),(RelIncl (bool L)) #) is strict RelStr
L is non empty antisymmetric lower-bounded upper-bounded bounded RelStr
Top L is Element of the carrier of L
the carrier of L is non empty set
"/\" ({},L) is Element of the carrier of L
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
a is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
P is Element of the carrier of L
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
L is non empty set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
Top (BoolePoset L) is Element of the carrier of (BoolePoset L)
the carrier of (BoolePoset L) is non empty set
"/\" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)
Bottom (BoolePoset L) is Element of the carrier of (BoolePoset L)
"\/" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)
L is non empty reflexive transitive antisymmetric lower-bounded non void RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
a is non empty filtered upper Element of bool the carrier of L
x is set
y is Element of the carrier of L
{{}} is non empty finite V35() set
BoolePoset {{}} is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
L is non empty non trivial reflexive transitive antisymmetric upper-bounded non void RelStr
the carrier of L is non empty non trivial set
bool the carrier of L is non empty set
Top L is Element of the carrier of L
"/\" ({},L) is Element of the carrier of L
uparrow (Top L) is non empty filtered upper Element of bool the carrier of L
{(Top L)} is non empty finite Element of bool the carrier of L
uparrow {(Top L)} is non empty upper Element of bool the carrier of L
a is non empty filtered upper Element of bool the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset L) is non empty set
a is Element of the carrier of (BoolePoset L)
'not' a is Element of the carrier of (BoolePoset L)
Bottom (BoolePoset L) is Element of the carrier of (BoolePoset L)
"\/" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)
a => (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)
a => is Relation-like Function-like V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) Element of bool [: the carrier of (BoolePoset L), the carrier of (BoolePoset L):]
[: the carrier of (BoolePoset L), the carrier of (BoolePoset L):] is non empty Relation-like set
bool [: the carrier of (BoolePoset L), the carrier of (BoolePoset L):] is non empty set
(a =>) . (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)
L \ a is Element of bool L
bool L is non empty set
bool L is non empty Element of bool (bool L)
bool (bool L) is non empty set
x is Element of the carrier of (BoolePoset L)
a "/\" x is Element of the carrier of (BoolePoset L)
a /\ x is set
a "\/" x is Element of the carrier of (BoolePoset L)
a \/ x is set
Top (BoolePoset L) is Element of the carrier of (BoolePoset L)
"/\" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset L) is non empty set
bool the carrier of (BoolePoset L) is non empty set
a is Element of bool the carrier of (BoolePoset L)
bool L is non empty Element of bool (bool L)
bool L is non empty set
bool (bool L) is non empty set
x is set
y is set
P is Element of the carrier of (BoolePoset L)
p is Element of the carrier of (BoolePoset L)
x is Element of the carrier of (BoolePoset L)
y is Element of the carrier of (BoolePoset L)
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset L) is non empty set
bool the carrier of (BoolePoset L) is non empty set
a is Element of bool the carrier of (BoolePoset L)
bool L is non empty Element of bool (bool L)
bool L is non empty set
bool (bool L) is non empty set
x is set
y is set
P is Element of the carrier of (BoolePoset L)
p is Element of the carrier of (BoolePoset L)
x is Element of the carrier of (BoolePoset L)
y is Element of the carrier of (BoolePoset L)
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset L) is non empty set
bool the carrier of (BoolePoset L) is non empty set
a is lower Element of bool the carrier of (BoolePoset L)
x is set
y is set
P is Element of the carrier of (BoolePoset L)
p is Element of the carrier of (BoolePoset L)
P "\/" p is Element of the carrier of (BoolePoset L)
x \/ y is set
x is Element of the carrier of (BoolePoset L)
y is Element of the carrier of (BoolePoset L)
x \/ y is set
x "\/" y is Element of the carrier of (BoolePoset L)
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset L) is non empty set
bool the carrier of (BoolePoset L) is non empty set
a is upper Element of bool the carrier of (BoolePoset L)
x is set
y is set
P is Element of the carrier of (BoolePoset L)
p is Element of the carrier of (BoolePoset L)
P "/\" p is Element of the carrier of (BoolePoset L)
x /\ y is set
x is Element of the carrier of (BoolePoset L)
y is Element of the carrier of (BoolePoset L)
x /\ y is set
x "/\" y is Element of the carrier of (BoolePoset L)
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset L) is non empty set
bool the carrier of (BoolePoset L) is non empty set
bool L is non empty set
bool (bool L) is non empty set
a is non empty lower Element of bool the carrier of (BoolePoset L)
x is finite Element of bool (bool L)
bool a is non empty set
P is finite Element of bool a
y is Element of bool the carrier of (BoolePoset L)
"\/" (y,(BoolePoset L)) is Element of the carrier of (BoolePoset L)
Bottom (BoolePoset L) is Element of the carrier of (BoolePoset L)
"\/" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)
union x is Element of bool L
bool L is non empty Element of bool (bool L)
x is finite Element of bool a
y is finite Element of bool (bool L)
P is finite Element of bool (bool L)
union P is Element of bool L
"\/" (x,(BoolePoset L)) is Element of the carrier of (BoolePoset L)
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset L) is non empty set
bool the carrier of (BoolePoset L) is non empty set
bool L is non empty set
bool (bool L) is non empty set
a is non empty upper Element of bool the carrier of (BoolePoset L)
Top (BoolePoset L) is Element of the carrier of (BoolePoset L)
"/\" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)
x is finite Element of bool (bool L)
bool a is non empty set
P is finite Element of bool a
y is Element of bool the carrier of (BoolePoset L)
"/\" (y,(BoolePoset L)) is Element of the carrier of (BoolePoset L)
meet y is set
Intersect x is Element of bool L
bool L is non empty Element of bool (bool L)
x is finite Element of bool a
y is finite Element of bool (bool L)
"/\" (x,(BoolePoset L)) is Element of the carrier of (BoolePoset L)
P is finite Element of bool (bool L)
meet P is Element of bool L
Intersect P is Element of bool L
L is non empty reflexive transitive antisymmetric non void with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is non empty reflexive transitive antisymmetric non void with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty directed lower Element of bool the carrier of L
x is non empty finite Element of bool the carrier of L
"/\" (x,L) is Element of the carrier of L
y is set
P is set
"/\" (P,L) is Element of the carrier of L
{y} is non empty finite set
P \/ {y} is non empty set
"/\" ((P \/ {y}),L) is Element of the carrier of L
p is Element of the carrier of L
{p} is non empty finite Element of bool the carrier of L
P \/ {p} is non empty set
"/\" ((P \/ {p}),L) is Element of the carrier of L
p is Element of the carrier of L
{p} is non empty finite Element of bool the carrier of L
"/\" ({p},L) is Element of the carrier of L
ax is finite Element of bool the carrier of L
"/\" (ax,L) is Element of the carrier of L
("/\" (ax,L)) "/\" ("/\" ({p},L)) is Element of the carrier of L
ay is Element of the carrier of L
ay is Element of the carrier of L
Y is Element of the carrier of L
ay is Element of the carrier of L
{ay} is non empty finite Element of bool the carrier of L
"/\" ({},L) is Element of the carrier of L
y is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
x "/\" y is Element of the carrier of L
{x,y} is non empty finite Element of bool the carrier of L
"/\" ({x,y},L) is Element of the carrier of L
P is Element of the carrier of L
L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L
a is Element of the carrier of L
x is Element of the carrier of L
a "/\" x is Element of the carrier of L
L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of L is non empty set
the InternalRel of L is non empty Relation-like Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
a is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of a is non empty set
the InternalRel of a is non empty Relation-like Element of bool [: the carrier of a, the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty Relation-like set
bool [: the carrier of a, the carrier of a:] is non empty set
RelStr(# the carrier of a, the InternalRel of a #) is strict RelStr
bool the carrier of L is non empty set
bool the carrier of a is non empty set
x is set
y is non empty directed lower (L) Element of bool the carrier of L
P is Element of bool the carrier of a
p is non empty directed lower Element of bool the carrier of a
ax is Element of the carrier of a
ay is Element of the carrier of a
ax "/\" ay is Element of the carrier of a
{ax,ay} is non empty finite Element of bool the carrier of a
"/\" ({ax,ay},a) is Element of the carrier of a
Y is Element of the carrier of L
F is Element of the carrier of L
{Y,F} is non empty finite Element of bool the carrier of L
Y "/\" F is Element of the carrier of L
"/\" ({Y,F},L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric non void with_suprema RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is non empty reflexive transitive antisymmetric non void with_suprema RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty filtered upper Element of bool the carrier of L
x is non empty finite Element of bool the carrier of L
"\/" (x,L) is Element of the carrier of L
y is set
P is set
"\/" (P,L) is Element of the carrier of L
{y} is non empty finite set
P \/ {y} is non empty set
"\/" ((P \/ {y}),L) is Element of the carrier of L
p is Element of the carrier of L
{p} is non empty finite Element of bool the carrier of L
P \/ {p} is non empty set
"\/" ((P \/ {p}),L) is Element of the carrier of L
p is Element of the carrier of L
{p} is non empty finite Element of bool the carrier of L
"\/" ({p},L) is Element of the carrier of L
ax is finite Element of bool the carrier of L
"\/" (ax,L) is Element of the carrier of L
("\/" (ax,L)) "\/" ("\/" ({p},L)) is Element of the carrier of L
ay is Element of the carrier of L
ay is Element of the carrier of L
Y is Element of the carrier of L
ay is Element of the carrier of L
{ay} is non empty finite Element of bool the carrier of L
"\/" ({},L) is Element of the carrier of L
y is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
x "\/" y is Element of the carrier of L
{x,y} is non empty finite Element of bool the carrier of L
"\/" ({x,y},L) is Element of the carrier of L
P is Element of the carrier of L
L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L
a is Element of the carrier of L
x is Element of the carrier of L
a "\/" x is Element of the carrier of L
L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of L is non empty set
the InternalRel of L is non empty Relation-like Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
a is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of a is non empty set
the InternalRel of a is non empty Relation-like Element of bool [: the carrier of a, the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty Relation-like set
bool [: the carrier of a, the carrier of a:] is non empty set
RelStr(# the carrier of a, the InternalRel of a #) is strict RelStr
bool the carrier of L is non empty set
bool the carrier of a is non empty set
x is set
y is non empty filtered upper (L) Element of bool the carrier of L
P is Element of bool the carrier of a
p is non empty filtered upper Element of bool the carrier of a
ax is Element of the carrier of a
ay is Element of the carrier of a
ax "\/" ay is Element of the carrier of a
{ax,ay} is non empty finite Element of bool the carrier of a
"\/" ({ax,ay},a) is Element of the carrier of a
Y is Element of the carrier of L
F is Element of the carrier of L
{Y,F} is non empty finite Element of bool the carrier of L
Y "\/" F is Element of the carrier of L
"\/" ({Y,F},L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L ~ is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of (L ~) is non empty set
bool the carrier of (L ~) is non empty set
a is set
x is non empty directed lower (L) Element of bool the carrier of L
y is non empty filtered upper Element of bool the carrier of (L ~)
P is Element of the carrier of (L ~)
p is Element of the carrier of (L ~)
P "\/" p is Element of the carrier of (L ~)
~ P is Element of the carrier of L
~ p is Element of the carrier of L
(~ P) "/\" (~ p) is Element of the carrier of L
x is non empty filtered upper (L ~ ) Element of bool the carrier of (L ~)
y is non empty directed lower Element of bool the carrier of L
P is Element of the carrier of L
p is Element of the carrier of L
P "/\" p is Element of the carrier of L
P ~ is Element of the carrier of (L ~)
p ~ is Element of the carrier of (L ~)
(P ~) "\/" (p ~) is Element of the carrier of (L ~)
L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L ~ is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of (L ~) is non empty set
bool the carrier of (L ~) is non empty set
a is set
(L ~) ~ is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the InternalRel of L is non empty Relation-like Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
RelStr(# the carrier of L, the InternalRel of L #) is strict RelStr
the carrier of ((L ~) ~) is non empty set
bool the carrier of ((L ~) ~) is non empty set
L is non empty reflexive transitive antisymmetric non void with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty directed lower Element of bool the carrier of L
a ` is Element of bool the carrier of L
the carrier of L \ a is set
y is Element of the carrier of L
P is Element of the carrier of L
y "/\" P is Element of the carrier of L
y is Element of the carrier of L
P is Element of the carrier of L
y is Element of the carrier of L
P is Element of the carrier of L
y "/\" P is Element of the carrier of L
L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
Ids L is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr
PRIME (InclPoset (Ids L)) is Element of bool the carrier of (InclPoset (Ids L))
the carrier of (InclPoset (Ids L)) is non empty set
bool the carrier of (InclPoset (Ids L)) is non empty set
a is non empty directed lower Element of bool the carrier of L
RelIncl (Ids L) is Relation-like V20( Ids L) V75() V78() V82() Element of bool [:(Ids L),(Ids L):]
[:(Ids L),(Ids L):] is non empty Relation-like set
bool [:(Ids L),(Ids L):] is non empty set
RelStr(# (Ids L),(RelIncl (Ids L)) #) is strict RelStr
y is Element of the carrier of (InclPoset (Ids L))
P is Element of the carrier of (InclPoset (Ids L))
p is Element of the carrier of (InclPoset (Ids L))
P "/\" p is Element of the carrier of (InclPoset (Ids L))
Y is non empty directed lower Element of bool the carrier of L
F is non empty directed lower Element of bool the carrier of L
P "/\" p is Element of the carrier of (InclPoset (Ids L))
ax is non empty directed lower Element of bool the carrier of L
ay is non empty directed lower Element of bool the carrier of L
ax /\ ay is Element of bool the carrier of L
Y is set
F is set
f is Element of the carrier of L
FF is Element of the carrier of L
f "/\" FF is Element of the carrier of L
P is Element of the carrier of L
p is Element of the carrier of L
P "/\" p is Element of the carrier of L
downarrow P is non empty directed lower Element of bool the carrier of L
{P} is non empty finite Element of bool the carrier of L
downarrow {P} is non empty lower Element of bool the carrier of L
downarrow p is non empty directed lower Element of bool the carrier of L
{p} is non empty finite Element of bool the carrier of L
downarrow {p} is non empty lower Element of bool the carrier of L
ax is non empty directed lower Element of bool the carrier of L
ay is non empty directed lower Element of bool the carrier of L
Y is Element of the carrier of (InclPoset (Ids L))
F is Element of the carrier of (InclPoset (Ids L))
Y /\ F is set
Y "/\" F is Element of the carrier of (InclPoset (Ids L))
f is set
FF is Element of the carrier of L
y is Element of the carrier of (InclPoset (Ids L))
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty filtered upper Element of bool the carrier of L
x is Element of the carrier of L
'not' x is Element of the carrier of L
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
x => (Bottom L) is Element of the carrier of L
x => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
(x =>) . (Bottom L) is Element of the carrier of L
x "\/" ('not' x) is Element of the carrier of L
Top L is Element of the carrier of L
"/\" ({},L) is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
x "\/" y is Element of the carrier of L
'not' x is Element of the carrier of L
x => (Bottom L) is Element of the carrier of L
x => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
(x =>) . (Bottom L) is Element of the carrier of L
'not' y is Element of the carrier of L
y => (Bottom L) is Element of the carrier of L
y => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
(y =>) . (Bottom L) is Element of the carrier of L
('not' x) "/\" ('not' y) is Element of the carrier of L
'not' (x "\/" y) is Element of the carrier of L
(x "\/" y) => (Bottom L) is Element of the carrier of L
(x "\/" y) => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
((x "\/" y) =>) . (Bottom L) is Element of the carrier of L
('not' (x "\/" y)) "/\" (x "\/" y) is Element of the carrier of L
L is set
BoolePoset L is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset L) is non empty set
bool the carrier of (BoolePoset L) is non empty set
bool L is non empty set
x is non empty filtered upper Element of bool the carrier of (BoolePoset L)
bool L is non empty Element of bool (bool L)
bool (bool L) is non empty set
InclPoset (bool L) is non empty strict reflexive transitive antisymmetric non void RelStr
RelIncl (bool L) is Relation-like V20( bool L) V75() V78() V82() Element of bool [:(bool L),(bool L):]
[:(bool L),(bool L):] is non empty Relation-like set
bool [:(bool L),(bool L):] is non empty set
RelStr(# (bool L),(RelIncl (bool L)) #) is strict RelStr
y is Element of bool L
P is Element of the carrier of (BoolePoset L)
'not' P is Element of the carrier of (BoolePoset L)
Bottom (BoolePoset L) is Element of the carrier of (BoolePoset L)
"\/" ({},(BoolePoset L)) is Element of the carrier of (BoolePoset L)
P => (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)
P => is Relation-like Function-like V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) Element of bool [: the carrier of (BoolePoset L), the carrier of (BoolePoset L):]
[: the carrier of (BoolePoset L), the carrier of (BoolePoset L):] is non empty Relation-like set
bool [: the carrier of (BoolePoset L), the carrier of (BoolePoset L):] is non empty set
(P =>) . (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)
L \ y is Element of bool L
y is Element of the carrier of (BoolePoset L)
'not' y is Element of the carrier of (BoolePoset L)
y => (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)
y => is Relation-like Function-like V21( the carrier of (BoolePoset L), the carrier of (BoolePoset L)) Element of bool [: the carrier of (BoolePoset L), the carrier of (BoolePoset L):]
(y =>) . (Bottom (BoolePoset L)) is Element of the carrier of (BoolePoset L)
L \ y is Element of bool L
L is non empty reflexive transitive antisymmetric non void RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L is non empty reflexive transitive antisymmetric non void RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty filtered upper Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric non void with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty filtered upper Element of bool the carrier of L
x is non empty finite Element of bool the carrier of L
a \/ x is non empty Element of bool the carrier of L
fininfs (a \/ x) is non empty filtered Element of bool the carrier of L
bool (a \/ x) is non empty set
{ ("/\" (b<sub>1</sub>,L)) where b<sub>1</sub> is finite Element of bool (a \/ x) : ex_inf_of b<sub>1</sub>,L } is set
uparrow (fininfs (a \/ x)) is non empty filtered upper Element of bool the carrier of L
"/\" (x,L) is Element of the carrier of L
y is Element of the carrier of L
the Element of a is Element of a
ax is Element of the carrier of L
ay is finite Element of bool (a \/ x)
"/\" (ay,L) is Element of the carrier of L
ay \ x is finite Element of bool (a \/ x)
Y is set
bool a is non empty set
Y is finite Element of bool a
F is finite Element of bool the carrier of L
F \/ x is non empty finite Element of bool the carrier of L
p is Element of the carrier of L
p "/\" ("/\" (x,L)) is Element of the carrier of L
"/\" (F,L) is Element of the carrier of L
("/\" (F,L)) "/\" ("/\" (x,L)) is Element of the carrier of L
FF is finite Element of bool the carrier of L
ay \/ x is non empty finite set
"/\" (FF,L) is Element of the carrier of L
f is finite Element of bool the carrier of L
"/\" (f,L) is Element of the carrier of L
"/\" ((F \/ x),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty filtered upper Element of bool the carrier of L
x is non empty filtered upper Element of bool the carrier of L
y is set
P is Element of the carrier of L
'not' P is Element of the carrier of L
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
P => (Bottom L) is Element of the carrier of L
P => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
(P =>) . (Bottom L) is Element of the carrier of L
P "\/" ('not' P) is Element of the carrier of L
Top L is Element of the carrier of L
"/\" ({},L) is Element of the carrier of L
P "/\" ('not' P) is Element of the carrier of L
ax is set
ay is Element of the carrier of L
x is Element of the carrier of L
'not' x is Element of the carrier of L
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
x => (Bottom L) is Element of the carrier of L
x => is Relation-like Function-like V21( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
(x =>) . (Bottom L) is Element of the carrier of L
{x} is non empty finite Element of bool the carrier of L
a \/ {x} is non empty Element of bool the carrier of L
fininfs (a \/ {x}) is non empty filtered Element of bool the carrier of L
bool (a \/ {x}) is non empty set
{ ("/\" (b<sub>1</sub>,L)) where b<sub>1</sub> is finite Element of bool (a \/ {x}) : ex_inf_of b<sub>1</sub>,L } is set
uparrow (fininfs (a \/ {x})) is non empty filtered upper Element of bool the carrier of L
"/\" ({x},L) is Element of the carrier of L
P is Element of the carrier of L
P "/\" ("/\" ({x},L)) is Element of the carrier of L
Top L is Element of the carrier of L
"/\" ({},L) is Element of the carrier of L
P "/\" (Top L) is Element of the carrier of L
x "\/" ('not' x) is Element of the carrier of L
P "/\" (x "\/" ('not' x)) is Element of the carrier of L
P "/\" x is Element of the carrier of L
P "/\" ('not' x) is Element of the carrier of L
(P "/\" x) "\/" (P "/\" ('not' x)) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric non void with_suprema RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty directed lower Element of bool the carrier of L
x is non empty finite Element of bool the carrier of L
a \/ x is non empty Element of bool the carrier of L
finsups (a \/ x) is non empty directed Element of bool the carrier of L
bool (a \/ x) is non empty set
{ ("\/" (b<sub>1</sub>,L)) where b<sub>1</sub> is finite Element of bool (a \/ x) : ex_sup_of b<sub>1</sub>,L } is set
downarrow (finsups (a \/ x)) is non empty directed lower Element of bool the carrier of L
"\/" (x,L) is Element of the carrier of L
y is Element of the carrier of L
the Element of a is Element of a
ax is Element of the carrier of L
ay is finite Element of bool (a \/ x)
"\/" (ay,L) is Element of the carrier of L
ay \ x is finite Element of bool (a \/ x)
Y is set
bool a is non empty set
Y is finite Element of bool a
F is finite Element of bool the carrier of L
F \/ x is non empty finite Element of bool the carrier of L
p is Element of the carrier of L
p "\/" ("\/" (x,L)) is Element of the carrier of L
"\/" (F,L) is Element of the carrier of L
("\/" (F,L)) "\/" ("\/" (x,L)) is Element of the carrier of L
FF is finite Element of bool the carrier of L
ay \/ x is non empty finite set
f is finite Element of bool the carrier of L
"\/" (f,L) is Element of the carrier of L
"\/" (FF,L) is Element of the carrier of L
"\/" ((F \/ x),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty directed lower Element of bool the carrier of L
x is non empty filtered upper Element of bool the carrier of L
{ b<sub>1</sub> where b<sub>1</sub> is non empty directed lower Element of bool the carrier of L : ( a c= b<sub>1</sub> & b<sub>1</sub> misses x ) } is set
P is set
p is non empty directed lower Element of bool the carrier of L
P is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
p is set
ax is non empty directed lower Element of bool the carrier of L
ax is Element of bool the carrier of L
p is Element of bool (bool the carrier of L)
ay is non empty directed lower Element of bool the carrier of L
union p is Element of bool the carrier of L
the Element of P is Element of P
ax is lower Element of bool the carrier of L
Y is Element of bool the carrier of L
F is Element of bool the carrier of L
Y \/ F is Element of bool the carrier of L
ay is Element of bool the carrier of L
Y is non empty directed lower Element of bool the carrier of L
Y is set
ay is non empty directed lower Element of bool the carrier of L
F is set
union P is set
P is set
p is non empty directed lower Element of bool the carrier of L
ax is Element of the carrier of L
ay is Element of the carrier of L
ax "/\" ay is Element of the carrier of L
{ay} is non empty finite Element of bool the carrier of L
p \/ {ay} is non empty Element of bool the carrier of L
finsups (p \/ {ay}) is non empty directed Element of bool the carrier of L
bool (p \/ {ay}) is non empty set
{ ("\/" (b<sub>1</sub>,L)) where b<sub>1</sub> is finite Element of bool (p \/ {ay}) : ex_sup_of b<sub>1</sub>,L } is set
downarrow (finsups (p \/ {ay})) is non empty directed lower Element of bool the carrier of L
F is set
{ax} is non empty finite Element of bool the carrier of L
p \/ {ax} is non empty Element of bool the carrier of L
finsups (p \/ {ax}) is non empty directed Element of bool the carrier of L
bool (p \/ {ax}) is non empty set
{ ("\/" (b<sub>1</sub>,L)) where b<sub>1</sub> is finite Element of bool (p \/ {ax}) : ex_sup_of b<sub>1</sub>,L } is set
downarrow (finsups (p \/ {ax})) is non empty directed lower Element of bool the carrier of L
FF is set
G is Element of the carrier of L
"\/" ({ax},L) is Element of the carrier of L
g is Element of the carrier of L
g "\/" ("\/" ({ax},L)) is Element of the carrier of L
gg is Element of the carrier of L
"\/" ({ay},L) is Element of the carrier of L
GG is Element of the carrier of L
GG "\/" ("\/" ({ay},L)) is Element of the carrier of L
g "\/" GG is Element of the carrier of L
GG "\/" g is Element of the carrier of L
(GG "\/" g) "\/" ax is Element of the carrier of L
g "\/" ax is Element of the carrier of L
GG "\/" (g "\/" ax) is Element of the carrier of L
(g "\/" GG) "\/" ax is Element of the carrier of L
(g "\/" GG) "\/" ay is Element of the carrier of L
GG "\/" ay is Element of the carrier of L
g "\/" (GG "\/" ay) is Element of the carrier of L
((g "\/" GG) "\/" ax) "/\" ((g "\/" GG) "\/" ay) is Element of the carrier of L
(g "\/" GG) "\/" (ax "/\" ay) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty directed lower Element of bool the carrier of L
x is Element of the carrier of L
y is set
uparrow x is non empty filtered upper Element of bool the carrier of L
{x} is non empty finite Element of bool the carrier of L
uparrow {x} is non empty upper Element of bool the carrier of L
P is Element of the carrier of L
y is non empty directed lower Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is non empty directed lower Element of bool the carrier of L
x is non empty filtered upper Element of bool the carrier of L
L ~ is non empty strict reflexive transitive antisymmetric distributive non void with_suprema with_infima RelStr
the carrier of (L ~) is non empty set
bool the carrier of (L ~) is non empty set
y is non empty directed lower Element of bool the carrier of (L ~)
P is non empty filtered upper Element of bool the carrier of (L ~)
p is non empty directed lower Element of bool the carrier of (L ~)
ax is non empty filtered upper Element of bool the carrier of L
L is non empty non trivial reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima RelStr
the carrier of L is non empty non trivial set
bool the carrier of L is non empty set
a is non empty proper filtered upper Element of bool the carrier of L
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
downarrow (Bottom L) is non empty directed lower Element of bool the carrier of L
{(Bottom L)} is non empty finite Element of bool the carrier of L
downarrow {(Bottom L)} is non empty lower Element of bool the carrier of L
y is set
x is non empty directed lower Element of bool the carrier of L
y is non empty filtered upper Element of bool the carrier of L
L is non empty set
BoolePoset L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset L) is non empty non trivial set
bool the carrier of (BoolePoset L) is non empty set
the non empty proper filtered upper Element of bool the carrier of (BoolePoset L) is non empty proper filtered upper Element of bool the carrier of (BoolePoset L)
x is non empty filtered upper Element of bool the carrier of (BoolePoset L)
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
BoolePoset the carrier of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset the carrier of L) is non empty non trivial set
bool the carrier of (BoolePoset the carrier of L) is non empty set
x is non empty proper filtered upper ( BoolePoset the carrier of L) Element of bool the carrier of (BoolePoset the carrier of L)
y is set
bool the carrier of L is non empty set
P is Element of bool the carrier of L
the carrier of L \ P is Element of bool the carrier of L
bool the carrier of L is non empty set
P is Element of bool the carrier of L
Bottom (BoolePoset the carrier of L) is Element of the carrier of (BoolePoset the carrier of L)
"\/" ({},(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)
p is set
ax is Element of the carrier of (BoolePoset the carrier of L)
ay is Element of the carrier of (BoolePoset the carrier of L)
ax "/\" ay is Element of the carrier of (BoolePoset the carrier of L)
P /\ p is Element of bool the carrier of L
L is non empty TopSpace-like TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
BoolePoset the carrier of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset the carrier of L) is non empty non trivial set
bool the carrier of (BoolePoset the carrier of L) is non empty set
y is Element of the carrier of (InclPoset the topology of L)
P is Element of the carrier of (InclPoset the topology of L)
bool the carrier of L is non empty Element of bool (bool the carrier of L)
InclPoset (bool the carrier of L) is non empty strict reflexive transitive antisymmetric non void RelStr
RelIncl (bool the carrier of L) is Relation-like V20( bool the carrier of L) V75() V78() V82() Element of bool [:(bool the carrier of L),(bool the carrier of L):]
[:(bool the carrier of L),(bool the carrier of L):] is non empty Relation-like set
bool [:(bool the carrier of L),(bool the carrier of L):] is non empty set
RelStr(# (bool the carrier of L),(RelIncl (bool the carrier of L)) #) is strict RelStr
RelIncl the topology of L is Relation-like V20( the topology of L) V75() V78() V82() Element of bool [: the topology of L, the topology of L:]
[: the topology of L, the topology of L:] is non empty Relation-like set
bool [: the topology of L, the topology of L:] is non empty set
RelStr(# the topology of L,(RelIncl the topology of L) #) is strict RelStr
ax is non empty proper filtered upper Element of bool the carrier of (BoolePoset the carrier of L)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of L : ( b<sub>1</sub> is open & not b<sub>1</sub> misses P & ex b<sub>2</sub> being set st
( b<sub>2</sub> in ax & b<sub>1</sub> misses b<sub>2</sub> ) ) } is set
Y is set
F is Element of bool the carrier of L
f is set
Y is Element of bool (bool the carrier of L)
F is Element of bool (bool the carrier of L)
union F is Element of bool the carrier of L
f is set
FF is Element of bool the carrier of L
G is set
f is Element of bool the carrier of L
FF is Element of bool the carrier of L
G is set
bool F is non empty set
f is finite Element of bool F
union f is set
FF is set
G is Element of bool the carrier of L
gg is set
FF is Relation-like Function-like set
dom FF is set
rng FF is set
G is Element of the carrier of (BoolePoset the carrier of L)
p is Element of the carrier of (BoolePoset the carrier of L)
p "/\" G is Element of the carrier of (BoolePoset the carrier of L)
the Element of p "/\" G is Element of p "/\" G
Bottom (BoolePoset the carrier of L) is Element of the carrier of (BoolePoset the carrier of L)
"\/" ({},(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)
p /\ G is set
g is set
FF . g is set
GG is Element of the carrier of (BoolePoset the carrier of L)
L is non empty TopSpace-like TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
BoolePoset the carrier of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset the carrier of L) is non empty non trivial set
bool the carrier of (BoolePoset the carrier of L) is non empty set
a is Element of the carrier of (InclPoset the topology of L)
x is Element of the carrier of (InclPoset the topology of L)
y is non empty proper filtered upper ( BoolePoset the carrier of L) Element of bool the carrier of (BoolePoset the carrier of L)
P is Element of the carrier of L
L is non empty TopSpace-like TopStruct
the topology of L is non empty Element of bool (bool the carrier of L)
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
BoolePoset the carrier of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
the carrier of (BoolePoset the carrier of L) is non empty non trivial set
bool the carrier of (BoolePoset the carrier of L) is non empty set
x is Element of the carrier of (InclPoset the topology of L)
y is Element of the carrier of (InclPoset the topology of L)
RelIncl the topology of L is Relation-like V20( the topology of L) V75() V78() V82() Element of bool [: the topology of L, the topology of L:]
[: the topology of L, the topology of L:] is non empty Relation-like set
bool [: the topology of L, the topology of L:] is non empty set
RelStr(# the topology of L,(RelIncl the topology of L) #) is strict RelStr
P is Element of bool the carrier of L
ax is Element of bool (bool the carrier of L)
union ax is Element of bool the carrier of L
bool ax is non empty set
{ (x \ b<sub>1</sub>) where b<sub>1</sub> is Element of bool the carrier of L : b<sub>1</sub> in ax } is set
the Element of ax is Element of ax
bool the carrier of L is non empty Element of bool (bool the carrier of L)
InclPoset (bool the carrier of L) is non empty strict reflexive transitive antisymmetric non void RelStr
RelIncl (bool the carrier of L) is Relation-like V20( bool the carrier of L) V75() V78() V82() Element of bool [:(bool the carrier of L),(bool the carrier of L):]
[:(bool the carrier of L),(bool the carrier of L):] is non empty Relation-like set
bool [:(bool the carrier of L),(bool the carrier of L):] is non empty set
RelStr(# (bool the carrier of L),(RelIncl (bool the carrier of L)) #) is strict RelStr
F is set
p is Element of bool the carrier of L
f is Element of bool the carrier of L
x \ f is Element of bool x
bool x is non empty set
F is Element of bool the carrier of (BoolePoset the carrier of L)
fininfs F is non empty filtered Element of bool the carrier of (BoolePoset the carrier of L)
bool F is non empty set
{ ("/\" (b<sub>1</sub>,(BoolePoset the carrier of L))) where b<sub>1</sub> is finite Element of bool F : ex_inf_of b<sub>1</sub>, BoolePoset the carrier of L } is set
uparrow (fininfs F) is non empty filtered upper Element of bool the carrier of (BoolePoset the carrier of L)
Bottom (BoolePoset the carrier of L) is Element of the carrier of (BoolePoset the carrier of L)
"\/" ({},(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)
FF is Element of the carrier of (BoolePoset the carrier of L)
G is finite Element of bool F
"/\" (G,(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)
g is set
GG is Element of bool the carrier of L
x \ GG is Element of bool x
bool x is non empty set
g is Relation-like Function-like set
dom g is set
rng g is set
Top (BoolePoset the carrier of L) is Element of the carrier of (BoolePoset the carrier of L)
"/\" ({},(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)
gg is Element of bool the carrier of (BoolePoset the carrier of L)
meet gg is set
GG is finite Element of bool ax
union GG is set
a is set
z is set
g . z is set
x \ (g . z) is Element of bool x
bool x is non empty set
FF is non empty filtered upper Element of bool the carrier of (BoolePoset the carrier of L)
G is Element of bool the carrier of L
x \ G is Element of bool x
bool x is non empty set
p is Element of bool the carrier of L
gg is Element of the carrier of L
g is set
GG is Element of bool the carrier of L
x \ GG is Element of bool x
GG /\ (x \ GG) is Element of bool x
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
the topology of L is non empty Element of bool (bool the carrier of L)
InclPoset the topology of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr
the carrier of (InclPoset the topology of L) is non empty non trivial set
a is open quasi_prebasis Element of bool (bool the carrier of L)
bool a is non empty set
FinMeetCl a is Element of bool (bool the carrier of L)
x is open quasi_basis Element of bool (bool the carrier of L)
BoolePoset the carrier of L is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete RelStr
p is Element of the carrier of (InclPoset the topology of L)
ax is Element of the carrier of (InclPoset the topology of L)
ay is Element of bool a
union ay is set
Y is Element of bool (bool the carrier of L)
F is Element of bool the carrier of L
bool ay is non empty set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
InclPoset (bool the carrier of L) is non empty strict reflexive transitive antisymmetric non void RelStr
RelIncl (bool the carrier of L) is Relation-like V20( bool the carrier of L) V75() V78() V82() Element of bool [:(bool the carrier of L),(bool the carrier of L):]
[:(bool the carrier of L),(bool the carrier of L):] is non empty Relation-like set
bool [:(bool the carrier of L),(bool the carrier of L):] is non empty set
RelStr(# (bool the carrier of L),(RelIncl (bool the carrier of L)) #) is strict RelStr
RelIncl the topology of L is Relation-like V20( the topology of L) V75() V78() V82() Element of bool [: the topology of L, the topology of L:]
[: the topology of L, the topology of L:] is non empty Relation-like set
bool [: the topology of L, the topology of L:] is non empty set
RelStr(# the topology of L,(RelIncl the topology of L) #) is strict RelStr
UniCl x is Element of bool (bool the carrier of L)
bool p is non empty set
the carrier of (BoolePoset the carrier of L) is non empty non trivial set
bool the carrier of (BoolePoset the carrier of L) is non empty set
F is non empty proper filtered upper ( BoolePoset the carrier of L) Element of bool the carrier of (BoolePoset the carrier of L)
f is set
Y is Element of bool the carrier of L
FF is Element of the carrier of L
G is Element of bool the carrier of L
gg is Element of bool (bool the carrier of L)
union gg is Element of bool the carrier of L
g is set
GG is Element of bool the carrier of L
a is Element of bool (bool the carrier of L)
Intersect a is Element of bool the carrier of L
bool F is non empty set
z is set
r is set
f is Relation-like Function-like set
dom f is set
rng f is set
FF is Element of bool a
union FF is set
G is set
f . G is set
bool FF is non empty set
G is finite Element of bool FF
union G is set
the Element of G is Element of G
g is Relation-like Function-like set
dom g is set
rng g is set
GG is set
a is set
g . a is set
z is Element of bool the carrier of L
r is set
f . r is set
the carrier of L \ z is Element of bool the carrier of L
p \ z is Element of bool p
ay is Element of bool the carrier of L
z ` is Element of bool the carrier of L
the carrier of L \ z is set
ay /\ (z `) is Element of bool the carrier of L
p /\ ( the carrier of L \ z) is Element of bool the carrier of L
Bottom (BoolePoset the carrier of L) is Element of the carrier of (BoolePoset the carrier of L)
"\/" ({},(BoolePoset the carrier of L)) is Element of the carrier of (BoolePoset the carrier of L)
a is set
GG is finite Element of bool (bool the carrier of L)
Intersect GG is Element of bool the carrier of L
z is set
g . z is set
p \ z is Element of bool p
z is set
g . the Element of G is set
p \ the Element of G is Element of bool p
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is Element of the carrier of L
x is Element of the carrier of L
y is non empty directed lower (L) Element of bool the carrier of L
"\/" (y,L) is Element of the carrier of L
y is non empty directed lower Element of bool the carrier of L
"\/" (y,L) is Element of the carrier of L
P is non empty directed lower Element of bool the carrier of L
"\/" (P,L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of L is non empty set
a is Element of the carrier of L
downarrow a is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{a} is non empty finite Element of bool the carrier of L
downarrow {a} is non empty lower Element of bool the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
x "/\" y is Element of the carrier of L
L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of L is non empty set
L is non empty reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of L is non empty set
a is Element of the carrier of L
downarrow a is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{a} is non empty finite Element of bool the carrier of L
downarrow {a} is non empty lower Element of bool the carrier of L
"\/" ((downarrow a),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is Element of the carrier of L
x is non empty directed lower (L) Element of bool the carrier of L
"\/" (x,L) is Element of the carrier of L
y is non empty finite Element of bool the carrier of L
"/\" (y,L) is Element of the carrier of L
waybelow a is non empty directed lower Element of bool the carrier of L
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of L : b<sub>1</sub> is_way_below a } is set
P is Element of the carrier of L
L is non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
Top L is Element of the carrier of L
"/\" ({},L) is Element of the carrier of L
bool the carrier of L is non empty set
a is Element of the carrier of L
downarrow a is non empty directed lower Element of bool the carrier of L
{a} is non empty finite Element of bool the carrier of L
downarrow {a} is non empty lower Element of bool the carrier of L
(downarrow a) ` is Element of bool the carrier of L
the carrier of L \ (downarrow a) is set
fininfs ((downarrow a) `) is non empty filtered Element of bool the carrier of L
bool ((downarrow a) `) is non empty set
{ ("/\" (b₁,L)) where b₁ is finite Element of bool ((downarrow a) `) : ex_inf_of b<sub>1</sub>,L } is set
uparrow (fininfs ((downarrow a) `)) is non empty filtered upper Element of bool the carrier of L
waybelow a is non empty directed lower Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : b₁ is_way_below a } is set
x is set
y is Element of the carrier of L
P is Element of the carrier of L
p is finite Element of bool ((downarrow a) `)
"/\" (p,L) is Element of the carrier of L
ax is finite Element of bool the carrier of L
ay is Element of the carrier of L
(downarrow a) /\ ((downarrow a) `) is Element of bool the carrier of L
ax is finite Element of bool the carrier of L
ax is finite Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous RelStr
Top L is Element of the carrier of L
the carrier of L is non empty set
"/\" ({},L) is Element of the carrier of L
bool the carrier of L is non empty set
downarrow (Top L) is non empty directed lower Element of bool the carrier of L
{(Top L)} is non empty finite Element of bool the carrier of L
downarrow {(Top L)} is non empty lower Element of bool the carrier of L
(downarrow (Top L)) ` is Element of bool the carrier of L
the carrier of L \ (downarrow (Top L)) is set
fininfs ((downarrow (Top L)) `) is non empty filtered Element of bool the carrier of L
bool ((downarrow (Top L)) `) is non empty set
{ ("/\" (b<sub>1</sub>,L)) where b<sub>1</sub> is finite Element of bool ((downarrow (Top L)) `) : ex_inf_of b₁,L } is set
uparrow (fininfs ((downarrow (Top L)) `)) is non empty filtered upper Element of bool the carrier of L
waybelow (Top L) is non empty directed lower Element of bool the carrier of L
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of L : b<sub>1</sub> is_way_below Top L } is set
a is Element of the carrier of L
a is non empty finite Element of bool the carrier of L
"/\" (a,L) is Element of the carrier of L
the Element of a is Element of a
y is Element of the carrier of L
P is Element of the carrier of L
a is Element of the carrier of L
L is non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
a is Element of the carrier of L
downarrow a is non empty directed lower Element of bool the carrier of L
{a} is non empty finite Element of bool the carrier of L
downarrow {a} is non empty lower Element of bool the carrier of L
(downarrow a) ` is Element of bool the carrier of L
the carrier of L \ (downarrow a) is set
fininfs ((downarrow a) `) is non empty filtered Element of bool the carrier of L
bool ((downarrow a) `) is non empty set
{ ("/\" (b₁,L)) where b₁ is finite Element of bool ((downarrow a) `) : ex_inf_of b<sub>1</sub>,L } is set
uparrow (fininfs ((downarrow a) `)) is non empty filtered upper Element of bool the carrier of L
waybelow a is non empty directed lower Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : b₁ is_way_below a } is set
x is non empty finite Element of bool the carrier of L
"/\" (x,L) is Element of the carrier of L
y is set
P is Element of the carrier of L
L is non empty reflexive transitive antisymmetric upper-bounded up-complete distributive non void with_suprema with_infima satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
a is Element of the carrier of L
downarrow a is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{a} is non empty finite Element of bool the carrier of L
downarrow {a} is non empty lower Element of bool the carrier of L
(downarrow a) ` is Element of bool the carrier of L
the carrier of L \ (downarrow a) is set
fininfs ((downarrow a) `) is non empty filtered Element of bool the carrier of L
bool ((downarrow a) `) is non empty set
{ ("/\" (b<sub>1</sub>,L)) where b<sub>1</sub> is finite Element of bool ((downarrow a) `) : ex_inf_of b₁,L } is set
uparrow (fininfs ((downarrow a) `)) is non empty filtered upper Element of bool the carrier of L
waybelow a is non empty directed lower Element of bool the carrier of L
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of L : b<sub>1</sub> is_way_below a } is set
"\/" ((downarrow a),L) is Element of the carrier of L
(uparrow (fininfs ((downarrow a) `))) ` is Element of bool the carrier of L
the carrier of L \ (uparrow (fininfs ((downarrow a) `))) is set
((downarrow a) `) ` is Element of bool the carrier of L
the carrier of L \ ((downarrow a) `) is set
P is non empty directed lower Element of bool the carrier of L
p is non empty directed lower (L) Element of bool the carrier of L
"\/" ((waybelow a),L) is Element of the carrier of L
"\/" (p,L) is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded non void with_suprema RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
x is Element of the carrier of L
a is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary Element of bool [: the carrier of L, the carrier of L:]
a -above x is Element of bool the carrier of L
bool the carrier of L is non empty set
y is Element of the carrier of L
P is Element of the carrier of L
[x,y] is Element of the carrier of [:L,L:]
[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema RelStr
the carrier of [:L,L:] is non empty set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V35() set
[x,P] is Element of the carrier of [:L,L:]
{x,P} is non empty finite set
{{x,P},{x}} is non empty finite V35() set
L is non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
a is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
a -above x is upper Element of bool the carrier of L
bool the carrier of L is non empty set
y is Element of the carrier of L
P is Element of the carrier of L
[x,y] is Element of the carrier of [:L,L:]
[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of [:L,L:] is non empty set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V35() set
[x,P] is Element of the carrier of [:L,L:]
{x,P} is non empty finite set
{{x,P},{x}} is non empty finite V35() set
y "/\" P is Element of the carrier of L
[x,(y "/\" P)] is Element of the carrier of [:L,L:]
{x,(y "/\" P)} is non empty finite set
{{x,(y "/\" P)},{x}} is non empty finite V35() set
x is Element of the carrier of L
y is Element of the carrier of L
[x,y] is Element of the carrier of [:L,L:]
[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of [:L,L:] is non empty set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V35() set
P is Element of the carrier of L
[x,P] is Element of the carrier of [:L,L:]
{x,P} is non empty finite set
{{x,P},{x}} is non empty finite V35() set
y "/\" P is Element of the carrier of L
[x,(y "/\" P)] is Element of the carrier of [:L,L:]
{x,(y "/\" P)} is non empty finite set
{{x,(y "/\" P)},{x}} is non empty finite V35() set
a -above x is upper Element of bool the carrier of L
y "/\" P is Element of the carrier of L
[x,(y "/\" P)] is Element of the carrier of [:L,L:]
{x,(y "/\" P)} is non empty finite set
{{x,(y "/\" P)},{x}} is non empty finite V35() set
L is non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
a is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
P is Element of the carrier of L
[x,P] is Element of the carrier of [:L,L:]
[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of [:L,L:] is non empty set
{x,P} is non empty finite set
{x} is non empty finite set
{{x,P},{x}} is non empty finite V35() set
y is Element of the carrier of L
p is Element of the carrier of L
[y,p] is Element of the carrier of [:L,L:]
{y,p} is non empty finite set
{y} is non empty finite set
{{y,p},{y}} is non empty finite V35() set
x "/\" y is Element of the carrier of L
[(x "/\" y),p] is Element of the carrier of [:L,L:]
{(x "/\" y),p} is non empty finite set
{(x "/\" y)} is non empty finite set
{{(x "/\" y),p},{(x "/\" y)}} is non empty finite V35() set
[(x "/\" y),P] is Element of the carrier of [:L,L:]
{(x "/\" y),P} is non empty finite set
{{(x "/\" y),P},{(x "/\" y)}} is non empty finite V35() set
P "/\" p is Element of the carrier of L
[(x "/\" y),(P "/\" p)] is Element of the carrier of [:L,L:]
{(x "/\" y),(P "/\" p)} is non empty finite set
{{(x "/\" y),(P "/\" p)},{(x "/\" y)}} is non empty finite V35() set
x is Element of the carrier of L
x "/\" x is Element of the carrier of L
y is Element of the carrier of L
[x,y] is Element of the carrier of [:L,L:]
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V35() set
P is Element of the carrier of L
[x,P] is Element of the carrier of [:L,L:]
{x,P} is non empty finite set
{{x,P},{x}} is non empty finite V35() set
y "/\" P is Element of the carrier of L
[x,(y "/\" P)] is Element of the carrier of [:L,L:]
{x,(y "/\" P)} is non empty finite set
{{x,(y "/\" P)},{x}} is non empty finite V35() set
L is non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr
a is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary Element of bool [: the carrier of L, the carrier of L:]
the carrier of [:L,L:] is non empty set
bool the carrier of [:L,L:] is non empty set
x is Element of bool the carrier of [:L,L:]
subrelstr x is strict reflexive transitive antisymmetric full SubRelStr of [:L,L:]
the carrier of (subrelstr x) is set
y is reflexive transitive antisymmetric full SubRelStr of [:L,L:]
the carrier of y is set
P is Element of the carrier of [:L,L:]
p is Element of the carrier of [:L,L:]
{P,p} is non empty finite Element of bool the carrier of [:L,L:]
"/\" ({P,p},[:L,L:]) is Element of the carrier of [:L,L:]
P `1 is Element of the carrier of L
P `2 is Element of the carrier of L
[(P `1),(P `2)] is Element of the carrier of [:L,L:]
{(P `1),(P `2)} is non empty finite set
{(P `1)} is non empty finite set
{{(P `1),(P `2)},{(P `1)}} is non empty finite V35() set
p `1 is Element of the carrier of L
p `2 is Element of the carrier of L
[(p `1),(p `2)] is Element of the carrier of [:L,L:]
{(p `1),(p `2)} is non empty finite set
{(p `1)} is non empty finite set
{{(p `1),(p `2)},{(p `1)}} is non empty finite V35() set
proj1 {P,p} is Element of bool the carrier of L
bool the carrier of L is non empty set
"/\" ((proj1 {P,p}),L) is Element of the carrier of L
proj2 {P,p} is Element of bool the carrier of L
"/\" ((proj2 {P,p}),L) is Element of the carrier of L
[("/\" ((proj1 {P,p}),L)),("/\" ((proj2 {P,p}),L))] is Element of the carrier of [:L,L:]
{("/\" ((proj1 {P,p}),L)),("/\" ((proj2 {P,p}),L))} is non empty finite set
{("/\" ((proj1 {P,p}),L))} is non empty finite set
{{("/\" ((proj1 {P,p}),L)),("/\" ((proj2 {P,p}),L))},{("/\" ((proj1 {P,p}),L))}} is non empty finite V35() set
{(P `1),(p `1)} is non empty finite Element of bool the carrier of L
"/\" ({(P `1),(p `1)},L) is Element of the carrier of L
[("/\" ({(P `1),(p `1)},L)),("/\" ((proj2 {P,p}),L))] is Element of the carrier of [:L,L:]
{("/\" ({(P `1),(p `1)},L)),("/\" ((proj2 {P,p}),L))} is non empty finite set
{("/\" ({(P `1),(p `1)},L))} is non empty finite set
{{("/\" ({(P `1),(p `1)},L)),("/\" ((proj2 {P,p}),L))},{("/\" ({(P `1),(p `1)},L))}} is non empty finite V35() set
{(P `2),(p `2)} is non empty finite Element of bool the carrier of L
"/\" ({(P `2),(p `2)},L) is Element of the carrier of L
[("/\" ({(P `1),(p `1)},L)),("/\" ({(P `2),(p `2)},L))] is Element of the carrier of [:L,L:]
{("/\" ({(P `1),(p `1)},L)),("/\" ({(P `2),(p `2)},L))} is non empty finite set
{{("/\" ({(P `1),(p `1)},L)),("/\" ({(P `2),(p `2)},L))},{("/\" ({(P `1),(p `1)},L))}} is non empty finite V35() set
(P `1) "/\" (p `1) is Element of the carrier of L
[((P `1) "/\" (p `1)),("/\" ({(P `2),(p `2)},L))] is Element of the carrier of [:L,L:]
{((P `1) "/\" (p `1)),("/\" ({(P `2),(p `2)},L))} is non empty finite set
{((P `1) "/\" (p `1))} is non empty finite set
{{((P `1) "/\" (p `1)),("/\" ({(P `2),(p `2)},L))},{((P `1) "/\" (p `1))}} is non empty finite V35() set
(P `2) "/\" (p `2) is Element of the carrier of L
[((P `1) "/\" (p `1)),((P `2) "/\" (p `2))] is Element of the carrier of [:L,L:]
{((P `1) "/\" (p `1)),((P `2) "/\" (p `2))} is non empty finite set
{{((P `1) "/\" (p `1)),((P `2) "/\" (p `2))},{((P `1) "/\" (p `1))}} is non empty finite V35() set
y is Element of the carrier of L
P is Element of the carrier of L
[y,P] is Element of the carrier of [:L,L:]
{y,P} is non empty finite set
{y} is non empty finite set
{{y,P},{y}} is non empty finite V35() set
p is Element of the carrier of L
[y,p] is Element of the carrier of [:L,L:]
{y,p} is non empty finite set
{{y,p},{y}} is non empty finite V35() set
P "/\" p is Element of the carrier of L
[y,(P "/\" p)] is Element of the carrier of [:L,L:]
{y,(P "/\" p)} is non empty finite set
{{y,(P "/\" p)},{y}} is non empty finite V35() set
{[y,P],[y,p]} is non empty Relation-like finite Element of bool the carrier of [:L,L:]
"/\" ({[y,P],[y,p]},[:L,L:]) is Element of the carrier of [:L,L:]
[y,P] "/\" [y,p] is Element of the carrier of [:L,L:]
proj1 {[y,P],[y,p]} is non empty finite Element of bool the carrier of L
bool the carrier of L is non empty set
"/\" ((proj1 {[y,P],[y,p]}),L) is Element of the carrier of L
proj2 {[y,P],[y,p]} is non empty finite Element of bool the carrier of L
"/\" ((proj2 {[y,P],[y,p]}),L) is Element of the carrier of L
[("/\" ((proj1 {[y,P],[y,p]}),L)),("/\" ((proj2 {[y,P],[y,p]}),L))] is Element of the carrier of [:L,L:]
{("/\" ((proj1 {[y,P],[y,p]}),L)),("/\" ((proj2 {[y,P],[y,p]}),L))} is non empty finite set
{("/\" ((proj1 {[y,P],[y,p]}),L))} is non empty finite set
{{("/\" ((proj1 {[y,P],[y,p]}),L)),("/\" ((proj2 {[y,P],[y,p]}),L))},{("/\" ((proj1 {[y,P],[y,p]}),L))}} is non empty finite V35() set
{y,y} is non empty finite Element of bool the carrier of L
"/\" ({y,y},L) is Element of the carrier of L
[("/\" ({y,y},L)),("/\" ((proj2 {[y,P],[y,p]}),L))] is Element of the carrier of [:L,L:]
{("/\" ({y,y},L)),("/\" ((proj2 {[y,P],[y,p]}),L))} is non empty finite set
{("/\" ({y,y},L))} is non empty finite set
{{("/\" ({y,y},L)),("/\" ((proj2 {[y,P],[y,p]}),L))},{("/\" ({y,y},L))}} is non empty finite V35() set
{P,p} is non empty finite Element of bool the carrier of L
"/\" ({P,p},L) is Element of the carrier of L
[("/\" ({y,y},L)),("/\" ({P,p},L))] is Element of the carrier of [:L,L:]
{("/\" ({y,y},L)),("/\" ({P,p},L))} is non empty finite set
{{("/\" ({y,y},L)),("/\" ({P,p},L))},{("/\" ({y,y},L))}} is non empty finite V35() set
y "/\" y is Element of the carrier of L
[(y "/\" y),("/\" ({P,p},L))] is Element of the carrier of [:L,L:]
{(y "/\" y),("/\" ({P,p},L))} is non empty finite set
{(y "/\" y)} is non empty finite set
{{(y "/\" y),("/\" ({P,p},L))},{(y "/\" y)}} is non empty finite V35() set
P "/\" p is Element of the carrier of L
[(y "/\" y),(P "/\" p)] is Element of the carrier of [:L,L:]
{(y "/\" y),(P "/\" p)} is non empty finite set
{{(y "/\" y),(P "/\" p)},{(y "/\" y)}} is non empty finite V35() set
[y,(P "/\" p)] is Element of the carrier of [:L,L:]
{y,(P "/\" p)} is non empty finite set
{{y,(P "/\" p)},{y}} is non empty finite V35() set
L is non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima RelStr
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
Ids L is non empty set
bool the carrier of L is non empty set
{ b₁ where b₁ is non empty directed lower Element of bool the carrier of L : verum } is set
InclPoset (Ids L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr
a is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary Element of bool [: the carrier of L, the carrier of L:]
a -below is Relation-like Function-like V21( the carrier of L, the carrier of (InclPoset (Ids L))) Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
the carrier of (InclPoset (Ids L)) is non empty set
[: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty Relation-like set
bool [: the carrier of L, the carrier of (InclPoset (Ids L)):] is non empty set
x is Element of the carrier of L
y is Element of the carrier of L
{x,y} is non empty finite Element of bool the carrier of L
(a -below) . y is Element of the carrier of (InclPoset (Ids L))
a -below y is non empty directed lower Element of bool the carrier of L
x "/\" y is Element of the carrier of L
a -below (x "/\" y) is non empty directed lower Element of bool the carrier of L
a -below x is non empty directed lower Element of bool the carrier of L
(a -below x) /\ (a -below y) is Element of bool the carrier of L
P is set
{ b₁ where b₁ is Element of the carrier of L : [b₁,(x "/\" y)] in a } is set
p is Element of the carrier of L
[p,(x "/\" y)] is Element of the carrier of [:L,L:]
[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of [:L,L:] is non empty set
{p,(x "/\" y)} is non empty finite set
{p} is non empty finite set
{{p,(x "/\" y)},{p}} is non empty finite V35() set
[p,y] is Element of the carrier of [:L,L:]
{p,y} is non empty finite set
{{p,y},{p}} is non empty finite V35() set
[p,x] is Element of the carrier of [:L,L:]
{p,x} is non empty finite set
{{p,x},{p}} is non empty finite V35() set
P is set
p is Element of the carrier of L
[p,y] is Element of the carrier of [:L,L:]
{p,y} is non empty finite set
{p} is non empty finite set
{{p,y},{p}} is non empty finite V35() set
[p,x] is Element of the carrier of [:L,L:]
{p,x} is non empty finite set
{{p,x},{p}} is non empty finite V35() set
[p,(x "/\" y)] is Element of the carrier of [:L,L:]
{p,(x "/\" y)} is non empty finite set
{{p,(x "/\" y)},{p}} is non empty finite V35() set
(a -below) . (x "/\" y) is Element of the carrier of (InclPoset (Ids L))
(a -below) . x is Element of the carrier of (InclPoset (Ids L))
((a -below) . x) "/\" ((a -below) . y) is Element of the carrier of (InclPoset (Ids L))
x is Element of the carrier of L
y is Element of the carrier of L
[x,y] is Element of the carrier of [:L,L:]
[:L,L:] is non empty strict reflexive transitive antisymmetric non void with_suprema with_infima RelStr
the carrier of [:L,L:] is non empty set
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V35() set
P is Element of the carrier of L
[x,P] is Element of the carrier of [:L,L:]
{x,P} is non empty finite set
{{x,P},{x}} is non empty finite V35() set
y "/\" P is Element of the carrier of L
[x,(y "/\" P)] is Element of the carrier of [:L,L:]
{x,(y "/\" P)} is non empty finite set
{{x,(y "/\" P)},{x}} is non empty finite V35() set
{y,P} is non empty finite Element of bool the carrier of L
y "/\" P is Element of the carrier of L
(a -below) . (y "/\" P) is Element of the carrier of (InclPoset (Ids L))
(a -below) . y is Element of the carrier of (InclPoset (Ids L))
(a -below) . P is Element of the carrier of (InclPoset (Ids L))
((a -below) . y) "/\" ((a -below) . P) is Element of the carrier of (InclPoset (Ids L))
((a -below) . y) /\ ((a -below) . P) is set
a -below P is non empty directed lower Element of bool the carrier of L
a -below y is non empty directed lower Element of bool the carrier of L
a -below (y "/\" P) is non empty directed lower Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
L -waybelow is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
a is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
x "/\" y is Element of the carrier of L
P is Element of the carrier of L
waybelow P is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : b₁ is_way_below P } is set
p is Element of the carrier of L
waybelow p is non empty directed lower Element of bool the carrier of L
{ b₁ where b₁ is Element of the carrier of L : b₁ is_way_below p } is set
P is Element of the carrier of L
p is Element of the carrier of L
[p,y] is Element of the carrier of [:L,L:]
[:L,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr
the carrier of [:L,L:] is non empty set
{p,y} is non empty finite set
{p} is non empty finite set
{{p,y},{p}} is non empty finite V35() set
[P,x] is Element of the carrier of [:L,L:]
{P,x} is non empty finite set
{P} is non empty finite set
{{P,x},{P}} is non empty finite V35() set
P "/\" p is Element of the carrier of L
[(P "/\" p),(x "/\" y)] is Element of the carrier of [:L,L:]
{(P "/\" p),(x "/\" y)} is non empty finite set
{(P "/\" p)} is non empty finite set
{{(P "/\" p),(x "/\" y)},{(P "/\" p)}} is non empty finite V35() set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
L -waybelow is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT Element of bool [: the carrier of L, the carrier of L:]
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
a is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
x "/\" y is Element of the carrier of L
{x,y} is non empty finite Element of bool the carrier of L
bool the carrier of L is non empty set
"/\" ({x,y},L) is Element of the carrier of L
P is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
L -waybelow is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT Element of bool [: the carrier of L, the carrier of L:]
the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
a is Element of the carrier of L
x is Element of the carrier of L
y is Element of the carrier of L
x "/\" y is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
L -waybelow is Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
a is Element of the carrier of L
x is Element of the carrier of L
[a,x] is Element of the carrier of [:L,L:]
[:L,L:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete RelStr
the carrier of [:L,L:] is non empty set
{a,x} is non empty finite set
{a} is non empty finite set
{{a,x},{a}} is non empty finite V35() set
y is Element of the carrier of L
[a,y] is Element of the carrier of [:L,L:]
{a,y} is non empty finite set
{{a,y},{a}} is non empty finite V35() set
x "/\" y is Element of the carrier of L
[a,(x "/\" y)] is Element of the carrier of [:L,L:]
{a,(x "/\" y)} is non empty finite set
{{a,(x "/\" y)},{a}} is non empty finite V35() set
P is set
waybelow (x "/\" y) is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{ b₁ where b₁ is Element of the carrier of L : b₁ is_way_below x "/\" y } is set
uparrow a is non empty filtered upper Element of bool the carrier of L
{a} is non empty finite Element of bool the carrier of L
uparrow {a} is non empty upper Element of bool the carrier of L
p is Element of the carrier of L
P is non empty directed lower Element of bool the carrier of L
"\/" (P,L) is Element of the carrier of L
"\/" ((waybelow (x "/\" y)),L) is Element of the carrier of L