K179() is Element of bool K175()
K175() is set
bool K175() is non empty set
K128() is set
bool K128() is non empty set
bool K179() is non empty set
K224() is set
{} is set
the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V56() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V56() set
{{}} is set
K202({{}}) is M10({{}})
[:K202({{}}),{{}}:] is Relation-like set
bool [:K202({{}}),{{}}:] is non empty set
PFuncs (K202({{}}),{{}}) is set
1 is non empty set
{{},1} is set
L is non empty reflexive 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
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
z is Element of the carrier of L
y is Element of the carrier of L
[z,y] is Element of [: the carrier of L, the carrier of L:]
{z,y} is set
{z} is set
{{z,y},{z}} is set
y9 is Element of the carrier of L
Y is Element of the carrier of L
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
y9 is Element of the carrier of L
Y is Element of the carrier of L
y9 is Element of the carrier of L
Y is Element of the carrier of L
L is RelStr
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
the carrier of L is set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is RelStr
the carrier of L is set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
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 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 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
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
L is non empty transitive antisymmetric lower-bounded 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
(L) is Relation-like Element of bool [: the carrier of L, the carrier of L:]
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
[x,z] is Element of [: the carrier of L, the carrier of L:]
y9 is Element of the carrier of L
x is Element of the carrier of L
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
y is Element of the carrier of L
[y9,y] is set
{y9,y} is set
{y9} is set
{{y9,y},{y9}} is set
[x,z] is Element of [: the carrier of L, 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, the carrier of L:]
{x,y} is set
{x} is set
{{x,y},{x}} is set
z is Element of the carrier of L
[z,y] is Element of [: the carrier of L, the carrier of L:]
{z,y} is set
{z} is set
{{z,y},{z}} is set
x "\/" z is Element of the carrier of L
[(x "\/" z),y] is Element of [: the carrier of L, the carrier of L:]
{(x "\/" z),y} is set
{(x "\/" z)} is set
{{(x "\/" z),y},{(x "\/" z)}} is set
x "\/" z is Element of the carrier of L
y9 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 is Element of the carrier of L
[(Bottom L),x] is Element of [: the carrier of L, the carrier of L:]
{(Bottom L),x} is set
{(Bottom L)} is set
{{(Bottom L),x},{(Bottom L)}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Relation-like (L) (L) Element of bool [: the carrier of L, 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, the carrier of L:]
{x,y} is set
{x} is set
{{x,y},{x}} is set
z is Element of the carrier of L
y9 is Element of the carrier of L
[z,y9] is Element of [: the carrier of L, the carrier of L:]
{z,y9} is set
{z} is set
{{z,y9},{z}} is set
x "\/" z is Element of the carrier of L
y "\/" y9 is Element of the carrier of L
[(x "\/" z),(y "\/" y9)] is Element of [: the carrier of L, the carrier of L:]
{(x "\/" z),(y "\/" y9)} is set
{(x "\/" z)} is set
{{(x "\/" z),(y "\/" y9)},{(x "\/" z)}} is set
[x,(y "\/" y9)] is Element of [: the carrier of L, the carrier of L:]
{x,(y "\/" y9)} is set
{{x,(y "\/" y9)},{x}} is set
[z,(y "\/" y9)] is Element of [: the carrier of L, the carrier of L:]
{z,(y "\/" y9)} is set
{{z,(y "\/" y9)},{z}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Relation-like (L) (L) Element of bool [: the carrier of L, the carrier of L:]
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
the carrier of L \/ the carrier of L is set
x is set
z is set
y is set
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
y9 is Element of the carrier of L
Y is Element of the carrier of L
u is Element of the carrier of L
y9 is Element of the carrier of L
y99 is Element of the carrier of L
Y is Element of the carrier of L
[x,y] is set
{x,y} is set
{{x,y},{x}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
L is RelStr
(L) is Relation-like Element of bool [: the carrier of L, the carrier of L:]
the carrier of L is set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
R is Element of the carrier of L
x is Element of the carrier of L
[R,x] is set
{R,x} is set
{R} is set
{{R,x},{R}} is set
L is transitive RelStr
(L) is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
the carrier of L is set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
y9 is Element of the carrier of L
x is Element of the carrier of L
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
y is Element of the carrier of L
[y9,y] is set
{y9,y} is set
{y9} is set
{{y9,y},{y9}} is set
L is non empty antisymmetric with_suprema RelStr
(L) is Relation-like (L) 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
the InternalRel of L is Relation-like Element of bool [: the carrier of L, 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, the carrier of L:]
{x,y} is set
{x} is set
{{x,y},{x}} is set
z is Element of the carrier of L
[z,y] is Element of [: the carrier of L, the carrier of L:]
{z,y} is set
{z} is set
{{z,y},{z}} is set
x "\/" z is Element of the carrier of L
[(x "\/" z),y] is Element of [: the carrier of L, the carrier of L:]
{(x "\/" z),y} is set
{(x "\/" z)} is set
{{(x "\/" z),y},{(x "\/" z)}} is set
x "\/" z is Element of the carrier of L
y9 is Element of the carrier of L
L is non empty antisymmetric lower-bounded RelStr
(L) is Relation-like (L) 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
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
x is Element of the carrier of L
[(Bottom L),x] is Element of [: the carrier of L, the carrier of L:]
{(Bottom L),x} is set
{(Bottom L)} is set
{{(Bottom L),x},{(Bottom L)}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
bool [: the carrier of L, the carrier of L:] is non empty Element of bool (bool [: the carrier of L, the carrier of L:])
bool (bool [: the carrier of L, the carrier of L:]) is non empty set
R is set
x is set
z is set
R is set
x is set
z is set
z is set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is set
(L) is Relation-like transitive (L) (L) (L) (L) (L) 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
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded 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
(L) is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
R is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
x is set
z is set
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
y is Element of the carrier of L
y9 is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded 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
(L) is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
R is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
x is set
z is set
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric RelStr
Top (InclPoset (L)) is Element of the carrier of (InclPoset (L))
the carrier of (InclPoset (L)) is non empty set
"/\" ({},(InclPoset (L))) is Element of the carrier of (InclPoset (L))
(L) is Relation-like transitive (L) (L) (L) (L) (L) 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
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
z is Element of the carrier of (InclPoset (L))
y is Element of the carrier of (InclPoset (L))
y9 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric RelStr
(L) is Relation-like transitive (L) (L) (L) (L) (L) 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
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
the carrier of (InclPoset (L)) is non empty set
x is Element of the carrier of (InclPoset (L))
z is Element of the carrier of (InclPoset (L))
y is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, 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
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
z is Element of the carrier of L
y is Element of the carrier of L
[z,y] is Element of [: the carrier of L, the carrier of L:]
{z,y} is set
{z} is set
{{z,y},{z}} is set
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
y9 is Element of the carrier of L
Y is Element of the carrier of L
[y9,Y] is Element of [: the carrier of L, the carrier of L:]
{y9,Y} is set
{y9} is set
{{y9,Y},{y9}} is set
y9 is Element of the carrier of L
Y is Element of the carrier of L
[y9,Y] is Element of [: the carrier of L, the carrier of L:]
{y9,Y} is set
{y9} is set
{{y9,Y},{y9}} is set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is Relation-like 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
x is Element of the carrier of L
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
[x,z] is Element of [: the carrier of L, the carrier of L:]
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
y9 is Element of the carrier of L
x is Element of the carrier of L
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
y is Element of the carrier of L
[y9,y] is set
{y9,y} is set
{y9} is set
{{y9,y},{y9}} is set
[x,z] is Element of [: the carrier of L, the carrier of L:]
Bottom 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, the carrier of L:]
{x,y} is set
{x} is set
{{x,y},{x}} is set
z is Element of the carrier of L
[z,y] is Element of [: the carrier of L, the carrier of L:]
{z,y} is set
{z} is set
{{z,y},{z}} is set
x "\/" z is Element of the carrier of L
[(x "\/" z),y] is Element of [: the carrier of L, the carrier of L:]
{(x "\/" z),y} is set
{(x "\/" z)} is set
{{(x "\/" z),y},{(x "\/" z)}} is set
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
x "\/" z 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 is Element of the carrier of L
[(Bottom L),x] is Element of [: the carrier of L, the carrier of L:]
{(Bottom L),x} is set
{(Bottom L)} is set
{{(Bottom L),x},{(Bottom L)}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
(L) is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
R is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
x is set
z is set
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
y is Element of the carrier of L
y9 is Element of the carrier of L
[y,y9] is Element of [: the carrier of L, the carrier of L:]
{y,y9} is set
{y} is set
{{y,y9},{y}} is set
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric upper-bounded RelStr
Bottom (InclPoset (L)) is Element of the carrier of (InclPoset (L))
the carrier of (InclPoset (L)) is non empty set
"\/" ({},(InclPoset (L))) is Element of the carrier of (InclPoset (L))
(L) is Relation-like transitive (L) (L) (L) (L) (L) 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
R is Element of the carrier of (InclPoset (L))
x is Element of the carrier of (InclPoset (L))
z is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric upper-bounded RelStr
(L) is Relation-like transitive (L) (L) (L) (L) (L) 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
the carrier of (InclPoset (L)) is non empty set
x is Element of the carrier of (InclPoset (L))
z is Element of the carrier of (InclPoset (L))
y is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
x is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
R /\ x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
z is Relation-like Element of bool [: the carrier of L, the carrier of L:]
y is Element of the carrier of L
y9 is Element of the carrier of L
[y,y9] is Element of [: the carrier of L, the carrier of L:]
{y,y9} is set
{y} is set
{{y,y9},{y}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
x is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
R /\ x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
z is Relation-like Element of bool [: the carrier of L, the carrier of L:]
u is Element of the carrier of L
y is Element of the carrier of L
y9 is Element of the carrier of L
[y,y9] is Element of [: the carrier of L, the carrier of L:]
{y,y9} is set
{y} is set
{{y,y9},{y}} is set
Y is Element of the carrier of L
[u,Y] is Element of [: the carrier of L, the carrier of L:]
{u,Y} is set
{u} is set
{{u,Y},{u}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
x is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
R /\ x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
z is Relation-like Element of bool [: the carrier of L, the carrier of L:]
y is Element of the carrier of L
Y is Element of the carrier of L
[y,Y] is Element of [: the carrier of L, the carrier of L:]
{y,Y} is set
{y} is set
{{y,Y},{y}} is set
y9 is Element of the carrier of L
[y9,Y] is Element of [: the carrier of L, the carrier of L:]
{y9,Y} is set
{y9} is set
{{y9,Y},{y9}} is set
y "\/" y9 is Element of the carrier of L
[(y "\/" y9),Y] is Element of [: the carrier of L, the carrier of L:]
{(y "\/" y9),Y} is set
{(y "\/" y9)} is set
{{(y "\/" y9),Y},{(y "\/" y9)}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
x is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
R /\ x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
z is Relation-like Element of bool [: the carrier of L, the carrier of L:]
y is Element of the carrier of L
[(Bottom L),y] is Element of [: the carrier of L, the carrier of L:]
{(Bottom L),y} is set
{(Bottom L)} is set
{{(Bottom L),y},{(Bottom L)}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
x is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
R /\ x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
z is Relation-like Element of bool [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() RelStr
the carrier of (InclPoset (L)) is non empty set
bool the carrier of (InclPoset (L)) is non empty set
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
R is non empty Element of bool the carrier of (InclPoset (L))
meet R is set
the Element of R is Element of R
z is Relation-like Element of bool [: the carrier of L, the carrier of L:]
y is Element of the carrier of L
y9 is Element of the carrier of L
[y,y9] is set
{y,y9} is set
{y} is set
{{y,y9},{y}} is set
[y,y9] is Element of [: the carrier of L, the carrier of L:]
u is Element of the carrier of L
y is Element of the carrier of L
y9 is Element of the carrier of L
[y,y9] is set
{y,y9} is set
{y} is set
{{y,y9},{y}} is set
Y is Element of the carrier of L
[u,Y] is set
{u,Y} is set
{u} is set
{{u,Y},{u}} is set
[y,y9] is Element of [: the carrier of L, the carrier of L:]
[u,Y] is Element of [: the carrier of L, the carrier of L:]
y9 is set
y is Element of the carrier of L
Y is Element of the carrier of L
[y,Y] is Element of [: the carrier of L, the carrier of L:]
{y,Y} is set
{y} is set
{{y,Y},{y}} is set
y9 is Element of the carrier of L
[y9,Y] is Element of [: the carrier of L, the carrier of L:]
{y9,Y} is set
{y9} is set
{{y9,Y},{y9}} is set
y "\/" y9 is Element of the carrier of L
[(y "\/" y9),Y] is Element of [: the carrier of L, the carrier of L:]
{(y "\/" y9),Y} is set
{(y "\/" y9)} is set
{{(y "\/" y9),Y},{(y "\/" y9)}} is set
y "\/" y9 is Element of the carrier of L
[(y "\/" y9),Y] is Element of [: the carrier of L, the carrier of L:]
{(y "\/" y9),Y} is set
{(y "\/" y9)} is set
{{(y "\/" y9),Y},{(y "\/" y9)}} is set
u is set
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
y is Element of the carrier of L
[(Bottom L),y] is Element of [: the carrier of L, the carrier of L:]
{(Bottom L),y} is set
{(Bottom L)} is set
{{(Bottom L),y},{(Bottom L)}} is set
y9 is set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() RelStr
R is set
x is set
R /\ x is set
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 with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() with_infima RelStr
the carrier of (InclPoset (L)) is non empty set
bool the carrier of (InclPoset (L)) is non empty set
R is Element of bool the carrier of (InclPoset (L))
meet R is set
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
z is Element of the carrier of (InclPoset (L))
y is Element of the carrier of (InclPoset (L))
y is Element of the carrier of (InclPoset (L))
y9 is set
Y is Element of the carrier of (InclPoset (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
R is Element of the carrier of L
x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
{ b1 where b1 is Element of the carrier of L : [b1,R] in x } is set
z is set
y is Element of the carrier of L
[y,R] is Element of [: the carrier of L, the carrier of L:]
{y,R} is set
{y} is set
{{y,R},{y}} is set
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [R,b1] in x } is set
z is set
y is Element of the carrier of L
[R,y] is Element of [: the carrier of L, the carrier of L:]
{R,y} is set
{R} is set
{{R,y},{R}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Element of the carrier of L
downarrow R is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{R} is Element of bool the carrier of L
downarrow {R} is lower Element of bool the carrier of L
x is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R,x) is Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,R] in x } is set
z is set
y is Element of the carrier of L
[y,R] is Element of [: the carrier of L, the carrier of L:]
{y,R} is set
{y} is set
{{y,R},{y}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Element of the carrier of L
x is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R,x) is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,R] in x } is set
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
[(Bottom L),R] is Element of [: the carrier of L, the carrier of L:]
{(Bottom L),R} is set
{(Bottom L)} is set
{{(Bottom L),R},{(Bottom L)}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Element of the carrier of L
x is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R,x) is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,R] in x } is set
y is Element of the carrier of L
y9 is Element of the carrier of L
[y9,R] is Element of [: the carrier of L, the carrier of L:]
{y9,R} is set
{y9} is set
{{y9,R},{y9}} is set
Y is Element of the carrier of L
[Y,R] is Element of [: the carrier of L, the carrier of L:]
{Y,R} is set
{Y} is set
{{Y,R},{Y}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Element of the carrier of L
x is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R,x) is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,R] in x } is set
y is Element of the carrier of L
y9 is Element of the carrier of L
y "\/" y9 is Element of the carrier of L
Y is Element of the carrier of L
[Y,R] is Element of [: the carrier of L, the carrier of L:]
{Y,R} is set
{Y} is set
{{Y,R},{Y}} is set
u is Element of the carrier of L
[u,R] is Element of [: the carrier of L, the carrier of L:]
{u,R} is set
{u} is set
{{u,R},{u}} is set
y9 is Element of the carrier of L
[y9,R] is Element of [: the carrier of L, the carrier of L:]
{y9,R} is set
{y9} is set
{{y9,R},{y9}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
R is Relation-like (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
(L,x,R) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,x] in R } is set
z is non empty directed lower Element of bool the carrier of L
x is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
z is Element of the carrier of L
x . z is Element of the carrier of (InclPoset (Ids L))
(L,z,R) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,z] in R } is set
x is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
z is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y is set
x . y is set
z . y is set
y9 is Element of the carrier of L
(L,y9,R) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,y9] in R } is set
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
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is set
z is Element of the carrier of L
(L,z,R) is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,z] in R } is set
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
y is Element of the carrier of L
[y,z] is Element of [: the carrier of L, the carrier of L:]
{y,z} is set
{y} is set
{{y,z},{y}} is set
y is Element of the carrier of L
[y,z] is Element of [: the carrier of L, the carrier of L:]
{y,z} is set
{y} is set
{{y,z},{y}} is set
y9 is Element of the carrier of L
[y9,z] is Element of [: the carrier of L, the carrier of L:]
{y9,z} is set
{y9} is set
{{y9,z},{y9}} is set
L is set
R is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of R is non empty set
[: the carrier of R, the carrier of R:] is non empty Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
x is Relation-like Element of bool [: the carrier of R, the carrier of R:]
z is Element of the carrier of R
(R,z,x) is Element of bool the carrier of R
bool the carrier of R is non empty set
{ b1 where b1 is Element of the carrier of R : [z,b1] in x } is set
[z,L] is set
{z,L} is set
{z} is set
{{z,L},{z}} is set
y is Element of the carrier of R
[z,y] is Element of [: the carrier of R, the carrier of R:]
{z,y} is set
{{z,y},{z}} is set
y is Element of the carrier of R
[z,y] is Element of [: the carrier of R, the carrier of R:]
{z,y} is set
{{z,y},{z}} is set
y9 is Element of the carrier of R
[z,y9] is Element of [: the carrier of R, the carrier of R:]
{z,y9} is set
{{z,y9},{z}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is set
z is Element of the carrier of L
downarrow z is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{z} is Element of bool the carrier of L
downarrow {z} is lower Element of bool the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
y is Element of the carrier of L
y is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded 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
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
R is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
(L,x,R) is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,x] in R } is set
downarrow x is non empty directed lower Element of bool the carrier of L
{x} is Element of bool the carrier of L
downarrow {x} is lower Element of bool the carrier of L
z is set
[z,x] is set
{z,x} is set
{z} is set
{{z,x},{z}} is set
L is non empty reflexive transitive antisymmetric RelStr
the carrier of L is non empty set
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 RelStr
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
PFuncs ( the carrier of L, the carrier of (InclPoset (Ids L))) is set
R is set
x is set
z is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
x is Relation-like Element of bool [:R,R:]
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
RelStr(# R,x #) is strict RelStr
the carrier of RelStr(# R,x #) is set
the InternalRel of RelStr(# R,x #) is Relation-like Element of bool [: the carrier of RelStr(# R,x #), the carrier of RelStr(# R,x #):]
[: the carrier of RelStr(# R,x #), the carrier of RelStr(# R,x #):] is Relation-like set
bool [: the carrier of RelStr(# R,x #), the carrier of RelStr(# R,x #):] is non empty set
z is set
y is set
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Y is set
u is set
[Y,u] is set
{Y,u} is set
{Y} is set
{{Y,u},{Y}} is set
y9 is set
Y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y99 is set
y2 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[y9,y99] is set
{y9,y99} is set
{y9} is set
{{y9,y99},{y9}} is set
R is strict RelStr
the carrier of R is set
the InternalRel of R is Relation-like Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
x is strict RelStr
the carrier of x is set
the InternalRel of x is Relation-like Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is Relation-like set
bool [: the carrier of x, the carrier of x:] is non empty set
z is set
y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
z is set
y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is strict RelStr
the carrier of L is non empty set
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
(InclPoset (Ids L)) |^ the carrier of L is non empty strict reflexive transitive antisymmetric with_suprema with_infima RelStr
the carrier of L --> (InclPoset (Ids L)) is non empty Relation-like the carrier of L -defined Function-like constant total quasi_total V86() RelStr-yielding Element of bool [: the carrier of L,{(InclPoset (Ids L))}:]
{(InclPoset (Ids L))} is set
[: the carrier of L,{(InclPoset (Ids L))}:] is Relation-like set
bool [: the carrier of L,{(InclPoset (Ids L))}:] is non empty set
the carrier of (L) is set
the carrier of ((InclPoset (Ids L)) |^ the carrier of L) is non empty set
x is set
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
z is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) is non empty functional FUNCTION_DOMAIN of the carrier of L, the carrier of (InclPoset (Ids L))
the InternalRel of (L) is Relation-like Element of bool [: the carrier of (L), the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is Relation-like set
bool [: the carrier of (L), the carrier of (L):] is non empty set
the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) is Relation-like Element of bool [: the carrier of ((InclPoset (Ids L)) |^ the carrier of L), the carrier of ((InclPoset (Ids L)) |^ the carrier of L):]
[: the carrier of ((InclPoset (Ids L)) |^ the carrier of L), the carrier of ((InclPoset (Ids L)) |^ the carrier of L):] is non empty Relation-like set
bool [: the carrier of ((InclPoset (Ids L)) |^ the carrier of L), the carrier of ((InclPoset (Ids L)) |^ the carrier of L):] is non empty set
x is set
z is set
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
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
y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
product ( the carrier of L --> (InclPoset (Ids L))) is strict RelStr
Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) is non empty functional FUNCTION_DOMAIN of the carrier of L, the carrier of (InclPoset (Ids L))
the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))) is set
u is Element of the carrier of (product ( the carrier of L --> (InclPoset (Ids L))))
Carrier ( the carrier of L --> (InclPoset (Ids L))) is Relation-like the carrier of L -defined Function-like total set
product (Carrier ( the carrier of L --> (InclPoset (Ids L)))) is set
y9 is Element of the carrier of (product ( the carrier of L --> (InclPoset (Ids L))))
y99 is set
( the carrier of L --> (InclPoset (Ids L))) . y99 is set
y . y99 is set
y9 . y99 is set
y2 is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of y2 is non empty set
Y is Element of the carrier of L
y . Y is Element of the carrier of (InclPoset (Ids L))
y9 . Y is Element of the carrier of (InclPoset (Ids L))
c13 is Element of the carrier of y2
b9 is Element of the carrier of y2
sb is Element of the carrier of L
y . sb is Element of the carrier of (InclPoset (Ids L))
y9 . sb is Element of the carrier of (InclPoset (Ids L))
tb is Element of the carrier of (InclPoset (Ids L))
j9 is Element of the carrier of (InclPoset (Ids L))
y99 is Relation-like Function-like set
Y is Relation-like Function-like set
the InternalRel of (product ( the carrier of L --> (InclPoset (Ids L)))) is Relation-like Element of bool [: the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))), the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))):]
[: the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))), the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))):] is Relation-like set
bool [: the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))), the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))):] is non empty set
the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) |_2 the carrier of (L) is Relation-like set
the InternalRel of ((InclPoset (Ids L)) |^ the carrier of L) /\ [: the carrier of (L), the carrier of (L):] is Relation-like set
z is set
y is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
product ( the carrier of L --> (InclPoset (Ids L))) is strict RelStr
the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))) is set
y9 is Element of the carrier of (product ( the carrier of L --> (InclPoset (Ids L))))
Y is Element of the carrier of (product ( the carrier of L --> (InclPoset (Ids L))))
[y9,Y] is set
{y9,Y} is set
{y9} is set
{{y9,Y},{y9}} is set
the InternalRel of (product ( the carrier of L --> (InclPoset (Ids L)))) is Relation-like Element of bool [: the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))), the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))):]
[: the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))), the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))):] is Relation-like set
bool [: the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))), the carrier of (product ( the carrier of L --> (InclPoset (Ids L)))):] is non empty set
Carrier ( the carrier of L --> (InclPoset (Ids L))) is Relation-like the carrier of L -defined Function-like total set
product (Carrier ( the carrier of L --> (InclPoset (Ids L)))) is set
u is Relation-like Function-like set
y9 is Relation-like Function-like set
the carrier of (InclPoset (Ids L)) is non empty set
Funcs ( the carrier of L, the carrier of (InclPoset (Ids L))) is non empty functional FUNCTION_DOMAIN of the carrier of L, the carrier of (InclPoset (Ids L))
[: 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
y99 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y2 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
c13 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
b9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
sb is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
tb is set
b9 . tb is set
sb . tb is set
j9 is Element of the carrier of L
b9 . j9 is Element of the carrier of (InclPoset (Ids L))
sb . j9 is Element of the carrier of (InclPoset (Ids L))
( the carrier of L --> (InclPoset (Ids L))) . j9 is RelStr
c18 is RelStr
the carrier of c18 is set
c19 is Element of the carrier of c18
c20 is Element of the carrier of c18
b9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
sb is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
z is Element of the carrier of L
(L,x,R) is lower Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,x] in R } is set
(L,z,R) is lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,z] in R } is set
y is set
y9 is Element of the carrier of L
[y9,x] is Element of [: the carrier of L, the carrier of L:]
{y9,x} is set
{y9} is set
{{y9,x},{y9}} is set
[y9,z] is Element of [: the carrier of L, the carrier of L:]
{y9,z} is set
{{y9,z},{y9}} is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
R is Relation-like (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R) is non empty Relation-like Function-like total quasi_total 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
z is Element of the carrier of L
y is Element of the carrier of L
(L,R) . z is set
(L,R) . y is set
(L,R) . z is Element of the carrier of (InclPoset (Ids L))
(L,z,R) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,z] in R } is set
(L,R) . y is Element of the carrier of (InclPoset (Ids L))
(L,y,R) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,y] in R } is set
y9 is Element of the carrier of (InclPoset (Ids L))
Y is Element of the carrier of (InclPoset (Ids L))
L is non empty reflexive transitive antisymmetric lower-bounded 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
(L) is strict RelStr
the carrier of (L) is set
R is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
z is Element of the carrier of L
(L,R) . z is Element of the carrier of (InclPoset (Ids L))
downarrow z is non empty directed lower Element of bool the carrier of L
{z} is Element of bool the carrier of L
downarrow {z} is lower Element of bool the carrier of L
(L,z,R) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,z] in R } is set
z is Element of the carrier of L
(L,R) . z is Element of the carrier of (InclPoset (Ids L))
downarrow z is non empty directed lower Element of bool the carrier of L
{z} is Element of bool the carrier of L
downarrow {z} is lower Element of bool the carrier of L
z is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is strict RelStr
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
IdsMap L is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
the carrier of L is non empty set
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
(L) is non empty strict RelStr
the carrier of (L) is non empty set
x is Element of the carrier of L
(IdsMap L) . x is Element of the carrier of (InclPoset (Ids L))
downarrow x is non empty directed lower Element of bool the carrier of L
{x} is Element of bool the carrier of L
downarrow {x} is lower Element of bool the carrier of L
x is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
L is non empty reflexive transitive antisymmetric lower-bounded 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
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
IdsMap L is non empty Relation-like Function-like total quasi_total monotone 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
R is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
x is set
(L,R) . x is set
(IdsMap L) . x is set
z is Element of the carrier of L
(L,R) . z is Element of the carrier of (InclPoset (Ids L))
(L,z,R) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,z] in R } is set
(IdsMap L) . z is Element of the carrier of (InclPoset (Ids L))
downarrow z is non empty directed lower Element of bool the carrier of L
{z} is Element of bool the carrier of L
downarrow {z} is lower Element of bool the carrier of L
y is Element of the carrier of (InclPoset (Ids L))
y9 is Element of the carrier of (InclPoset (Ids L))
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is non empty directed lower Element of bool the carrier of L
the Element of R is Element of R
L is non empty reflexive transitive antisymmetric upper-bounded RelStr
the carrier of L is non empty 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
R is non empty filtered upper Element of bool the carrier of L
the Element of R is Element of R
L is non empty reflexive transitive antisymmetric lower-bounded RelStr
Bottom L is Element of the carrier of L
the carrier of L is non empty set
"\/" ({},L) is Element of the carrier of L
downarrow (Bottom L) is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{(Bottom L)} is Element of bool the carrier of L
downarrow {(Bottom L)} is lower Element of bool the carrier of L
R is set
{ b1 where b1 is Element of the carrier of L : ex b2 being Element of the carrier of L st
( b1 <= b2 & b2 in {(Bottom L)} ) } is set
x is Element of the carrier of L
z is Element of the carrier of L
z is Element of the carrier of L
R is set
L is non empty reflexive transitive antisymmetric upper-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
uparrow (Top L) is non empty filtered upper Element of bool the carrier of L
bool the carrier of L is non empty set
{(Top L)} is Element of bool the carrier of L
uparrow {(Top L)} is upper Element of bool the carrier of L
R is set
x is Element of the carrier of L
R is set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema 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
{(Bottom L)} is Element of bool the carrier of L
R is non empty directed lower Element of bool the carrier of L
x is set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema 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
{(Bottom L)} is Element of bool the carrier of L
the carrier of L --> {(Bottom L)} is non empty Relation-like the carrier of L -defined bool the carrier of L -valued Function-like constant total quasi_total Element of bool [: the carrier of L,(bool the carrier of L):]
[: the carrier of L,(bool the carrier of L):] is non empty Relation-like set
bool [: the carrier of L,(bool the carrier of L):] is non empty set
Ids L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
downarrow (Bottom L) is non empty directed lower Element of bool the carrier of L
downarrow {(Bottom L)} is lower Element of bool the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
the carrier of L is non empty set
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
{(Bottom L)} is Element of bool the carrier of L
the carrier of L --> {(Bottom L)} is non empty Relation-like the carrier of L -defined bool the carrier of L -valued Function-like constant total quasi_total Element of bool [: the carrier of L,(bool the carrier of L):]
[: the carrier of L,(bool the carrier of L):] is non empty Relation-like set
bool [: the carrier of L,(bool the carrier of L):] is non empty set
R is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
x is Element of the carrier of L
z is Element of the carrier of L
R . x is set
R . z is set
R . x is Element of the carrier of (InclPoset (Ids L))
R . z is Element of the carrier of (InclPoset (Ids L))
y is Element of the carrier of (InclPoset (Ids L))
y9 is Element of the carrier of (InclPoset (Ids L))
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema 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
{(Bottom L)} is Element of bool the carrier of L
the carrier of L --> {(Bottom L)} is non empty Relation-like the carrier of L -defined bool the carrier of L -valued Function-like constant total quasi_total Element of bool [: the carrier of L,(bool the carrier of L):]
[: the carrier of L,(bool the carrier of L):] is non empty Relation-like set
bool [: the carrier of L,(bool the carrier of L):] is non empty set
(L) is non empty strict RelStr
the carrier of (L) is non empty set
Ids L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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 non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
z is Element of the carrier of L
x . z is Element of the carrier of (InclPoset (Ids L))
downarrow z is non empty directed lower Element of bool the carrier of L
{z} is Element of bool the carrier of L
downarrow {z} is lower Element of bool the carrier of L
z is Element of the carrier of L
x . z is Element of the carrier of (InclPoset (Ids L))
downarrow z is non empty directed lower Element of bool the carrier of L
{z} is Element of bool the carrier of L
downarrow {z} is lower Element of bool the carrier of L
x is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
L is non empty reflexive transitive antisymmetric lower-bounded 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
bool the carrier of L is non empty set
[: the carrier of L,(bool the carrier of L):] is non empty Relation-like set
bool [: the carrier of L,(bool the carrier of L):] is non empty set
Ids L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
{(Bottom L)} is Element of bool the carrier of L
the carrier of L --> {(Bottom L)} is non empty Relation-like the carrier of L -defined bool the carrier of L -valued Function-like constant total quasi_total Element of bool [: the carrier of L,(bool the carrier of L):]
(L) is non empty strict RelStr
the InternalRel of (L) is Relation-like 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
R is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[( the carrier of L --> {(Bottom L)}),(L,R)] is Element of [:(bool [: the carrier of L,(bool the carrier of L):]),(bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]):]
[:(bool [: the carrier of L,(bool the carrier of L):]),(bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]):] is non empty Relation-like set
{( the carrier of L --> {(Bottom L)}),(L,R)} is functional set
{( the carrier of L --> {(Bottom L)})} is functional set
{{( the carrier of L --> {(Bottom L)}),(L,R)},{( the carrier of L --> {(Bottom L)})}} is set
y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y9 is set
y . y9 is set
(L,R) . y9 is set
Y is Element of the carrier of L
(L,Y,R) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,Y] in R } is set
(L,R) . Y is Element of the carrier of (InclPoset (Ids L))
u is non empty directed lower Element of bool the carrier of L
y . Y is Element of the carrier of (InclPoset (Ids L))
y9 is Element of the carrier of (InclPoset (Ids L))
y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty strict RelStr
the carrier of (L) is non empty set
IdsMap L is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
the carrier of L is non empty set
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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)
z is Element of the carrier of (L)
y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y9 is set
y . y9 is set
(IdsMap L) . y9 is set
Y is Element of the carrier of L
downarrow Y is non empty directed lower Element of bool the carrier of L
{Y} is Element of bool the carrier of L
downarrow {Y} is lower Element of bool the carrier of L
y . Y is Element of the carrier of (InclPoset (Ids L))
(IdsMap L) . Y is Element of the carrier of (InclPoset (Ids L))
u is Element of the carrier of (InclPoset (Ids L))
y9 is Element of the carrier of (InclPoset (Ids L))
[z,x] is Element of [: the carrier of (L), the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is non empty Relation-like set
{z,x} is set
{z} is set
{{z,x},{z}} is set
the InternalRel of (L) is Relation-like Element of bool [: the carrier of (L), the carrier of (L):]
bool [: the carrier of (L), the carrier of (L):] is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty strict RelStr
the carrier of (L) is non empty set
R is Element of the carrier of (L)
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset (L)) is non empty set
(L) is non empty strict upper-bounded RelStr
the carrier of (L) is non empty set
[: the carrier of (InclPoset (L)), the carrier of (L):] is non empty Relation-like set
bool [: the carrier of (InclPoset (L)), the carrier of (L):] is non empty set
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
R is set
x is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,x) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
R is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (InclPoset (L)), the carrier of (L):]
x is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
R . x is set
(L,x) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
z is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,z) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
x is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
R . x is set
(L,x) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
R is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (InclPoset (L)), the carrier of (L):]
x is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (InclPoset (L)), the carrier of (L):]
dom R is non empty set
dom x is non empty set
z is set
y is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
R . y is set
(L,y) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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 . y is set
R . z is set
x . z is set
L is non empty reflexive transitive antisymmetric lower-bounded 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
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
R is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
x is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R) is non empty Relation-like Function-like total quasi_total monotone 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
(L,x) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
z is set
(L,R) . z is set
(L,x) . z is set
y is Element of the carrier of L
(L,y,R) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,y] in R } is set
(L,y,x) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,y] in x } is set
y9 is set
Y is Element of the carrier of L
[Y,y] is Element of [: the carrier of L, the carrier of L:]
{Y,y} is set
{Y} is set
{{Y,y},{Y}} is set
(L,R) . y is Element of the carrier of (InclPoset (Ids L))
(L,x) . y is Element of the carrier of (InclPoset (Ids L))
y9 is Element of the carrier of (InclPoset (Ids L))
Y is Element of the carrier of (InclPoset (Ids L))
L is non empty reflexive transitive antisymmetric lower-bounded 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
R is Element of the carrier of L
x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
z is Relation-like Element of bool [: the carrier of L, the carrier of L:]
(L,R,x) is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,R] in x } is set
(L,R,z) is Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,R] in z } is set
y is set
y9 is Element of the carrier of L
[y9,R] is Element of [: the carrier of L, the carrier of L:]
{y9,R} is set
{y9} is set
{{y9,R},{y9}} is set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
(L) is non empty strict upper-bounded RelStr
(L) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (InclPoset (L)), the carrier of (L):]
the carrier of (InclPoset (L)) is non empty set
the carrier of (L) is non empty set
[: the carrier of (InclPoset (L)), the carrier of (L):] is non empty Relation-like set
bool [: the carrier of (InclPoset (L)), the carrier of (L):] is non empty set
R is Element of the carrier of (InclPoset (L))
x is Element of the carrier of (InclPoset (L))
(L) . R is set
(L) . x is set
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
y9 is Element of the carrier of (L)
Y is Element of the carrier of (L)
(L) . R is Element of the carrier of (L)
(L) . x is Element of the carrier of (L)
z is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,z) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
y is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,y) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
u is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y99 is set
u . y99 is set
y9 . y99 is set
Y is Element of the carrier of L
(L,Y,z) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,Y] in z } is set
(L,Y,y) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,Y] in y } is set
u . Y is Element of the carrier of (InclPoset (Ids L))
y9 . Y is Element of the carrier of (InclPoset (Ids L))
y2 is Element of the carrier of (InclPoset (Ids L))
c13 is Element of the carrier of (InclPoset (Ids L))
[(L,z),(L,y)] is Element of [:(bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]),(bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]):]
[:(bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]),(bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]):] is non empty Relation-like set
{(L,z),(L,y)} is functional set
{(L,z)} is functional set
{{(L,z),(L,y)},{(L,z)}} is set
the InternalRel of (L) is 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
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
(L) is non empty strict upper-bounded RelStr
(L) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (InclPoset (L)), the carrier of (L):]
the carrier of (InclPoset (L)) is non empty set
the carrier of (L) is non empty set
[: the carrier of (InclPoset (L)), the carrier of (L):] is non empty Relation-like set
bool [: the carrier of (InclPoset (L)), the carrier of (L):] is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty strict upper-bounded RelStr
the carrier of (L) is non empty set
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset (L)) is non empty set
[: the carrier of (L), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (L), the carrier of (InclPoset (L)):] is non empty set
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
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
R is set
x is Relation-like Element of bool [: the carrier of L, the carrier of L:]
z is Relation-like Element of bool [: the carrier of L, the carrier of L:]
y is Element of the carrier of L
y9 is Element of the carrier of L
[y,y9] is set
{y,y9} is set
{y} is set
{{y,y9},{y}} is set
[y,y9] is Element of [: the carrier of L, the carrier of L:]
Y is Element of the carrier of L
u is Element of the carrier of L
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y9 . u is Element of the carrier of (InclPoset (Ids L))
y9 . y9 is Element of the carrier of (InclPoset (Ids L))
downarrow y9 is non empty directed lower Element of bool the carrier of L
{y9} is Element of bool the carrier of L
downarrow {y9} is lower Element of bool the carrier of L
y99 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
u is Element of the carrier of L
y is Element of the carrier of L
y9 is Element of the carrier of L
[y,y9] is set
{y,y9} is set
{y} is set
{{y,y9},{y}} is set
Y is Element of the carrier of L
[u,Y] is set
{u,Y} is set
{u} is set
{{u,Y},{u}} is set
[y,y9] is Element of [: the carrier of L, the carrier of L:]
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y9 . y9 is Element of the carrier of (InclPoset (Ids L))
y9 . Y is Element of the carrier of (InclPoset (Ids L))
y99 is Element of the carrier of (InclPoset (Ids L))
Y is Element of the carrier of (InclPoset (Ids L))
y2 is non empty directed lower Element of bool the carrier of L
c13 is Element of the carrier of L
b9 is Element of the carrier of L
sb is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
sb . b9 is Element of the carrier of (InclPoset (Ids L))
y is Element of the carrier of L
Y is Element of the carrier of L
[y,Y] is Element of [: the carrier of L, the carrier of L:]
{y,Y} is set
{y} is set
{{y,Y},{y}} is set
y9 is Element of the carrier of L
[y9,Y] is Element of [: the carrier of L, the carrier of L:]
{y9,Y} is set
{y9} is set
{{y9,Y},{y9}} is set
y "\/" y9 is Element of the carrier of L
[(y "\/" y9),Y] is Element of [: the carrier of L, the carrier of L:]
{(y "\/" y9),Y} is set
{(y "\/" y9)} is set
{{(y "\/" y9),Y},{(y "\/" y9)}} is set
u is Element of the carrier of L
y9 is Element of the carrier of L
y99 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y99 . y9 is Element of the carrier of (InclPoset (Ids L))
y99 . Y is Element of the carrier of (InclPoset (Ids L))
Y is non empty directed lower Element of bool the carrier of L
y2 is Element of the carrier of L
c13 is Element of the carrier of L
b9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
b9 . c13 is Element of the carrier of (InclPoset (Ids L))
y2 is Element of the carrier of L
y "\/" y9 is Element of the carrier of L
c13 is Element of the carrier of L
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
y is Element of the carrier of L
[(Bottom L),y] is Element of [: the carrier of L, the carrier of L:]
{(Bottom L),y} is set
{(Bottom L)} is set
{{(Bottom L),y},{(Bottom L)}} is set
u is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Y is Element of the carrier of L
u . Y is Element of the carrier of (InclPoset (Ids L))
y9 is non empty directed lower Element of bool the carrier of L
y9 is Element of the carrier of L
y is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
y9 is set
Y is set
[y9,Y] is set
{y9,Y} is set
{y9} is set
{{y9,Y},{y9}} is set
y99 is Element of the carrier of L
u is set
Y is Element of the carrier of L
y9 is set
y2 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y2 . Y is Element of the carrier of (InclPoset (Ids L))
[u,y9] is set
{u,y9} is set
{u} is set
{{u,y9},{u}} is set
y9 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
R is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
x is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
z is set
x . z is set
y is Element of the carrier of (L)
x . y is Element of the carrier of (InclPoset (L))
y9 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
Y is set
u is set
[Y,u] is set
{Y,u} is set
{Y} is set
{{Y,u},{Y}} is set
Y is Element of the carrier of L
y9 is set
y2 is Element of the carrier of L
y99 is set
c13 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
c13 . y2 is Element of the carrier of (InclPoset (Ids L))
[y9,y99] is set
{y9,y99} is set
{y9} is set
{{y9,y99},{y9}} is set
b9 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
R is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
x is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
dom R is non empty set
dom x is non empty set
z is set
R . z is set
x . z is set
y is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
y9 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
Y is set
u is set
[Y,u] is set
{Y,u} is set
{Y} is set
{{Y,u},{Y}} is set
y9 is Element of the carrier of L
y99 is Element of the carrier of L
Y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Y . y99 is Element of the carrier of (InclPoset (Ids L))
y9 is Element of the carrier of L
y99 is Element of the carrier of L
Y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Y . y99 is Element of the carrier of (InclPoset (Ids L))
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty strict upper-bounded RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
(L) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
the carrier of (L) is non empty set
the carrier of (InclPoset (L)) is non empty set
[: the carrier of (L), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (L), the carrier of (InclPoset (L)):] is non empty set
RelIncl (L) is Relation-like reflexive antisymmetric transitive total quasi_total Element of bool [:(L),(L):]
[:(L),(L):] is non empty Relation-like set
bool [:(L),(L):] is non empty set
RelStr(# (L),(RelIncl (L)) #) is strict RelStr
x is Element of the carrier of (L)
z is Element of the carrier of (L)
(L) . x is set
(L) . z is set
[x,z] is Element of [: the carrier of (L), the carrier of (L):]
[: the carrier of (L), the carrier of (L):] is non empty Relation-like set
{x,z} is set
{x} is set
{{x,z},{x}} is set
the InternalRel of (L) is Relation-like Element of bool [: the carrier of (L), the carrier of (L):]
bool [: the carrier of (L), the carrier of (L):] is non empty set
the carrier of L is non empty set
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
(L) . y is set
(L) . y9 is 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
Y is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
u is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
Y is set
y2 is set
[Y,y2] is set
{Y,y2} is set
{Y} is set
{{Y,y2},{Y}} is set
b9 is Element of the carrier of L
y . b9 is Element of the carrier of (InclPoset (Ids L))
y9 . b9 is Element of the carrier of (InclPoset (Ids L))
y . y2 is set
y9 . y2 is set
sb is Element of the carrier of (InclPoset (Ids L))
tb is Element of the carrier of (InclPoset (Ids L))
j9 is Element of the carrier of (InclPoset (Ids L))
c18 is Element of the carrier of (InclPoset (Ids L))
(L) . x is Element of the carrier of (InclPoset (L))
c13 is Element of the carrier of L
j9 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L) . z is Element of the carrier of (InclPoset (L))
j9 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
c18 is Element of the carrier of L
c19 is Element of the carrier of L
c20 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
c20 . c19 is Element of the carrier of (InclPoset (Ids L))
y9 is Element of the carrier of (InclPoset (L))
y99 is Element of the carrier of (InclPoset (L))
[y9,y99] is Element of [: the carrier of (InclPoset (L)), the carrier of (InclPoset (L)):]
[: the carrier of (InclPoset (L)), the carrier of (InclPoset (L)):] is non empty Relation-like set
{y9,y99} is set
{y9} is set
{{y9,y99},{y9}} is set
Y is Element of the carrier of (InclPoset (L))
y2 is Element of the carrier of (InclPoset (L))
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty strict upper-bounded RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
(L) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
the carrier of (L) is non empty set
the carrier of (InclPoset (L)) is non empty set
[: the carrier of (L), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (L), the carrier of (InclPoset (L)):] is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset (L)) is non empty set
(L) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of (InclPoset (L)), the carrier of (L):]
(L) is non empty strict upper-bounded RelStr
the carrier of (L) is non empty set
[: the carrier of (InclPoset (L)), the carrier of (L):] is non empty Relation-like set
bool [: the carrier of (InclPoset (L)), the carrier of (L):] is non empty set
dom (L) is non empty set
(L) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
[: the carrier of (L), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (L), the carrier of (InclPoset (L)):] is non empty set
(L) * (L) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (InclPoset (L)), the carrier of (InclPoset (L)):]
[: the carrier of (InclPoset (L)), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (InclPoset (L)), the carrier of (InclPoset (L)):] is non empty set
id (dom (L)) is non empty Relation-like dom (L) -defined dom (L) -valued Function-like one-to-one total quasi_total Element of bool [:(dom (L)),(dom (L)):]
[:(dom (L)),(dom (L)):] is non empty Relation-like set
bool [:(dom (L)),(dom (L)):] is non empty set
dom ((L) * (L)) is non empty set
dom (id (dom (L))) is non empty Element of bool (dom (L))
bool (dom (L)) is non empty set
z is set
((L) * (L)) . z is set
(id (dom (L))) . z is set
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
y is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L) . y is set
(L) . ((L) . y) is set
(L,y) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
(L) . (L,y) is set
y9 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
Y is set
u is set
[Y,u] is set
{Y,u} is set
{Y} is set
{{Y,u},{Y}} is set
y9 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
y9 is Element of the carrier of L
y99 is Element of the carrier of L
Y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Y . y99 is Element of the carrier of (InclPoset (Ids L))
(L,y99,y) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,y99] in y } is set
y9 is Element of the carrier of L
y99 is Element of the carrier of L
(L,y99,y) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,y99] in y } is set
(L,y) . y99 is Element of the carrier of (InclPoset (Ids L))
Y is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty strict upper-bounded RelStr
the carrier of (L) is non empty set
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset (L)) is non empty set
(L) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
[: the carrier of (L), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (L), the carrier of (InclPoset (L)):] is non empty set
(L) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of (InclPoset (L)), the carrier of (L):]
[: the carrier of (InclPoset (L)), the carrier of (L):] is non empty Relation-like set
bool [: the carrier of (InclPoset (L)), the carrier of (L):] is non empty set
(L) * (L) is non empty Relation-like Function-like total quasi_total 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
id the carrier of (L) is non empty Relation-like the carrier of (L) -defined the carrier of (L) -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of (L), the carrier of (L):]
dom ((L) * (L)) is non empty set
dom (id the carrier of (L)) is non empty Element of bool the carrier of (L)
bool the carrier of (L) is non empty set
z is set
((L) * (L)) . z is set
(id the carrier of (L)) . z is set
the carrier of L is non empty set
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
((L) * (L)) . y is set
y9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
(L) . y is 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
dom (L) is non empty set
u is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L) . u is set
(L,u) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
dom y9 is non empty set
dom y is non empty set
y9 is set
y9 . y9 is set
y . y9 is set
Y is set
y99 is Element of the carrier of L
(L,y99,u) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,y99] in u } is set
[Y,y99] is set
{Y,y99} is set
{Y} is set
{{Y,y99},{Y}} is set
y2 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
y2 is Element of the carrier of L
c13 is Element of the carrier of L
b9 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
b9 . c13 is Element of the carrier of (InclPoset (Ids L))
Y is set
c13 is non empty directed lower Element of bool the carrier of L
y2 is Element of the carrier of L
y99 is Element of the carrier of L
[y2,y99] is Element of [: the carrier of L, the carrier of L:]
{y2,y99} is set
{y2} is set
{{y2,y99},{y2}} is set
c13 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,y99,u) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,y99] in u } is set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of (InclPoset (L)), the carrier of (L):]
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset (L)) is non empty set
(L) is non empty strict upper-bounded RelStr
the carrier of (L) is non empty set
[: the carrier of (InclPoset (L)), the carrier of (L):] is non empty Relation-like set
bool [: the carrier of (InclPoset (L)), the carrier of (L):] is non empty set
dom (L) is non empty set
id (dom (L)) is non empty Relation-like dom (L) -defined dom (L) -valued Function-like one-to-one total quasi_total Element of bool [:(dom (L)),(dom (L)):]
[:(dom (L)),(dom (L)):] is non empty Relation-like set
bool [:(dom (L)),(dom (L)):] is non empty set
(L) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
[: the carrier of (L), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (L), the carrier of (InclPoset (L)):] is non empty set
(L) * (L) is Relation-like Function-like set
R is Relation-like Function-like set
(L) * R is Relation-like Function-like set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty Relation-like Function-like one-to-one total quasi_total monotone Element of bool [: the carrier of (InclPoset (L)), the carrier of (L):]
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset (L)) is non empty set
(L) is non empty strict upper-bounded RelStr
the carrier of (L) is non empty set
[: the carrier of (InclPoset (L)), the carrier of (L):] is non empty Relation-like set
bool [: the carrier of (InclPoset (L)), the carrier of (L):] is non empty set
(L) " is Relation-like Function-like one-to-one set
(L) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
[: the carrier of (L), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (L), the carrier of (InclPoset (L)):] is non empty set
(L) * (L) is non empty Relation-like Function-like total quasi_total 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
id the carrier of (L) is non empty Relation-like the carrier of (L) -defined the carrier of (L) -valued Function-like one-to-one total quasi_total Element of bool [: the carrier of (L), the carrier of (L):]
rng (L) is non empty set
dom (L) is non empty set
dom (L) is non empty set
(L) * (L) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (InclPoset (L)), the carrier of (InclPoset (L)):]
[: the carrier of (InclPoset (L)), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (InclPoset (L)), the carrier of (InclPoset (L)):] is non empty set
id (dom (L)) is non empty Relation-like dom (L) -defined dom (L) -valued Function-like one-to-one total quasi_total Element of bool [:(dom (L)),(dom (L)):]
[:(dom (L)),(dom (L)):] is non empty Relation-like set
bool [:(dom (L)),(dom (L)):] is non empty set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
(L) is non empty strict upper-bounded RelStr
(L) is non empty Relation-like Function-like one-to-one total quasi_total monotone Element of bool [: the carrier of (InclPoset (L)), the carrier of (L):]
the carrier of (InclPoset (L)) is non empty set
the carrier of (L) is non empty set
[: the carrier of (InclPoset (L)), the carrier of (L):] is non empty Relation-like set
bool [: the carrier of (InclPoset (L)), the carrier of (L):] is non empty set
[: the carrier of (L), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (L), the carrier of (InclPoset (L)):] is non empty set
(L) " is Relation-like Function-like one-to-one set
(L) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
R is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
R is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
R is Element of the carrier of L
{ b1 where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
meet { b1 where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
waybelow R is non empty directed lower Element of bool the carrier of L
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
z is set
y is non empty directed lower Element of bool the carrier of L
"\/" (y,L) is Element of the carrier of L
downarrow R is non empty directed lower Element of bool the carrier of L
{R} is Element of bool the carrier of L
downarrow {R} is lower Element of bool the carrier of L
"\/" ((downarrow R),L) is Element of the carrier of L
y is set
z is Element of bool (bool the carrier of L)
meet z is Element of bool 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
y9 is Element of the carrier of L
y is set
{ b1 where b1 is Element of the carrier of L : b1 is_way_below R } is set
y9 is set
Y is non empty directed lower Element of bool the carrier of L
"\/" (Y,L) is Element of the carrier of L
u is Element of the carrier of L
L is non empty reflexive transitive antisymmetric 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
{ b1 where b1 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 with_infima RelStr
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
R is non empty directed lower Element of bool the carrier of L
"\/" (R,L) is Element of the carrier of L
x is Relation-like Function-like set
dom x is set
z is set
y is Element of the carrier of L
x . y is set
y9 is set
downarrow y is non empty directed lower Element of bool the carrier of L
{y} is Element of bool the carrier of L
downarrow {y} is lower Element of bool the carrier of L
(downarrow y) /\ R is Element of bool the carrier of L
downarrow y is non empty directed lower Element of bool the carrier of L
{y} is Element of bool the carrier of L
downarrow {y} is lower Element of bool the carrier of L
Y is Element of the carrier of L
downarrow Y is non empty directed lower Element of bool the carrier of L
{Y} is Element of bool the carrier of L
downarrow {Y} is lower Element of bool the carrier of L
(downarrow Y) /\ R is Element of bool the carrier of L
z is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y9 is Element of the carrier of L
y . y9 is Element of the carrier of (InclPoset (Ids L))
downarrow y9 is non empty directed lower Element of bool the carrier of L
{y9} is Element of bool the carrier of L
downarrow {y9} is lower Element of bool the carrier of L
(downarrow y9) /\ R is Element of bool the carrier of L
Y is Element of the carrier of L
y . Y is Element of the carrier of (InclPoset (Ids L))
downarrow Y is non empty directed lower Element of bool the carrier of L
{Y} is Element of bool the carrier of L
downarrow {Y} is lower Element of bool the carrier of L
x is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
z is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
dom x is non empty set
dom z is non empty set
y is set
y9 is Element of the carrier of L
x . y9 is Element of the carrier of (InclPoset (Ids L))
downarrow y9 is non empty directed lower Element of bool the carrier of L
{y9} is Element of bool the carrier of L
downarrow {y9} is lower Element of bool the carrier of L
(downarrow y9) /\ R is Element of bool the carrier of L
z . y9 is Element of the carrier of (InclPoset (Ids L))
x . y is set
z . y is set
L is non empty reflexive transitive antisymmetric 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
{ b1 where b1 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 with_infima RelStr
R is non empty directed lower Element of bool the carrier of L
(L,R) is non empty Relation-like Function-like total quasi_total 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
z is Element of the carrier of L
(L,R) . x is set
(L,R) . z is set
"\/" (R,L) is Element of the carrier of L
(L,R) . x is Element of the carrier of (InclPoset (Ids L))
downarrow x is non empty directed lower Element of bool the carrier of L
{x} is Element of bool the carrier of L
downarrow {x} is lower Element of bool the carrier of L
(downarrow x) /\ R is Element of bool the carrier of L
(L,R) . z is Element of the carrier of (InclPoset (Ids L))
downarrow z is non empty directed lower Element of bool the carrier of L
{z} is Element of bool the carrier of L
downarrow {z} is lower Element of bool the carrier of L
(downarrow z) /\ R is Element of bool the carrier of L
y is Element of the carrier of (InclPoset (Ids L))
y9 is Element of the carrier of (InclPoset (Ids L))
"\/" (R,L) is Element of the carrier of L
(L,R) . x is Element of the carrier of (InclPoset (Ids L))
downarrow x is non empty directed lower Element of bool the carrier of L
{x} is Element of bool the carrier of L
downarrow {x} is lower Element of bool the carrier of L
(downarrow x) /\ R is Element of bool the carrier of L
(L,R) . z is Element of the carrier of (InclPoset (Ids L))
downarrow z is non empty directed lower Element of bool the carrier of L
{z} is Element of bool the carrier of L
downarrow {z} is lower Element of bool the carrier of L
y is Element of the carrier of (InclPoset (Ids L))
y9 is Element of the carrier of (InclPoset (Ids L))
"\/" (R,L) is Element of the carrier of L
y is Element of the carrier of (InclPoset (Ids L))
y9 is Element of the carrier of (InclPoset (Ids L))
"\/" (R,L) is Element of the carrier of L
(L,R) . x is Element of the carrier of (InclPoset (Ids L))
downarrow x is non empty directed lower Element of bool the carrier of L
{x} is Element of bool the carrier of L
downarrow {x} is lower Element of bool the carrier of L
(L,R) . z is Element of the carrier of (InclPoset (Ids L))
downarrow z is non empty directed lower Element of bool the carrier of L
{z} is Element of bool the carrier of L
downarrow {z} is lower Element of bool the carrier of L
y is Element of the carrier of (InclPoset (Ids L))
y9 is Element of the carrier of (InclPoset (Ids L))
"\/" (R,L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric 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
{ b1 where b1 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 with_infima RelStr
the carrier of (InclPoset (Ids L)) is non empty set
R is Element of the carrier of L
downarrow R is non empty directed lower Element of bool the carrier of L
{R} is Element of bool the carrier of L
downarrow {R} is lower Element of bool the carrier of L
x is non empty directed lower Element of bool the carrier of L
(L,x) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[: 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
(L,x) . R is Element of the carrier of (InclPoset (Ids L))
"\/" (x,L) is Element of the carrier of L
(downarrow R) /\ x is Element of bool the carrier of L
"\/" (x,L) is Element of the carrier of L
"\/" (x,L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
(L) is strict RelStr
the carrier of (L) is set
R is non empty directed lower Element of bool the carrier of L
(L,R) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Ids L is non empty set
{ b1 where b1 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 with_infima RelStr
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 non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
z is Element of the carrier of L
x . z is Element of the carrier of (InclPoset (Ids L))
downarrow z is non empty directed lower Element of bool the carrier of L
{z} is Element of bool the carrier of L
downarrow {z} is lower Element of bool the carrier of L
z is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
L is non empty reflexive antisymmetric with_infima RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
R is Element of the carrier of L
{R} is Element of bool the carrier of L
downarrow R is non empty directed Element of bool the carrier of L
downarrow {R} is Element of bool the carrier of L
x is non empty lower Element of bool the carrier of L
{R} "/\" x is Element of bool the carrier of L
(downarrow R) /\ x is Element of bool the carrier of L
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of L : ( b1 in {R} & b2 in x ) } is set
z is set
y is Element of the carrier of L
y9 is Element of the carrier of L
y "/\" y9 is Element of the carrier of L
u is Element of the carrier of L
u is Element of the carrier of L
Y is Element of the carrier of L
z is set
y is Element of x
y "/\" R 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 RelStr
the carrier of L is non empty set
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 RelStr
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
L is non empty reflexive transitive antisymmetric lower-bounded up-complete with_infima satisfying_MC meet-continuous RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
R is non empty directed lower Element of bool the carrier of L
(L,R) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Ids L is non empty set
{ b1 where b1 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 with_infima RelStr
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
(L,R) . x is Element of the carrier of (InclPoset (Ids L))
y is non empty directed lower Element of bool the carrier of L
downarrow x is non empty directed lower Element of bool the carrier of L
{x} is Element of bool the carrier of L
downarrow {x} is lower Element of bool the carrier of L
(downarrow x) /\ R is Element of bool the carrier of L
"\/" (R,L) is Element of the carrier of L
"\/" (y,L) is Element of the carrier of L
y9 is Element of bool the carrier of L
"\/" (y9,L) is Element of the carrier of L
{x} "/\" R is Element of bool the carrier of L
"\/" (({x} "/\" R),L) is Element of the carrier of L
x "/\" ("\/" (R,L)) is Element of the carrier of L
"\/" (R,L) is Element of the carrier of L
"\/" (y,L) is Element of the carrier of L
"\/" ((downarrow x),L) is Element of the carrier of L
"\/" (R,L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
R is Element of the carrier of L
{R} is Element of bool the carrier of L
x is directed Element of bool the carrier of L
{R} "/\" x is Element of bool the carrier of L
"\/" (({R} "/\" x),L) is Element of the carrier of L
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of L : ( b1 in {R} & b2 in x ) } is set
z is Element of the carrier of L
y is Element of the carrier of L
y9 is Element of the carrier of L
y "/\" y9 is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
x is Element of the carrier of L
R is non empty directed Element of bool the carrier of L
"\/" (R,L) is Element of the carrier of L
waybelow x is non empty directed lower Element of bool the carrier of L
{x} is Element of bool the carrier of L
{x} "/\" R is Element of bool the carrier of L
"\/" (({x} "/\" R),L) is Element of the carrier of L
downarrow ("\/" (({x} "/\" R),L)) is non empty directed lower Element of bool the carrier of L
{("\/" (({x} "/\" R),L))} is Element of bool the carrier of L
downarrow {("\/" (({x} "/\" R),L))} is lower Element of bool the carrier of L
z is set
{ b1 where b1 is Element of the carrier of L : b1 is_way_below x } is set
y is Element of the carrier of L
y9 is Element of the carrier of L
x "/\" y9 is Element of the carrier of L
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of L : ( b1 in {x} & b2 in R ) } is set
{x,y9} is Element of bool the carrier of L
"\/" ((waybelow x),L) is Element of the carrier of L
"\/" ((downarrow ("\/" (({x} "/\" R),L))),L) is Element of the carrier of L
R is Element of the carrier of L
x is non empty directed Element of bool the carrier of L
"\/" (x,L) is Element of the carrier of L
{R} is Element of bool the carrier of L
{R} "/\" x is Element of bool the carrier of L
"\/" (({R} "/\" x),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
R is non empty directed lower Element of bool the carrier of L
(L,R) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
Ids L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
L is non empty reflexive antisymmetric RelStr
(L) is Relation-like 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
R is Element of the carrier of L
x is Element of the carrier of L
[R,x] is set
{R,x} is set
{R} is set
{{R,x},{R}} is set
[R,x] is Element of [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive RelStr
(L) is Relation-like 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
y9 is Element of the carrier of L
x is Element of the carrier of L
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
y is Element of the carrier of L
[y9,y] is set
{y9,y} is set
{y9} is set
{{y9,y},{y9}} is set
[x,z] is Element of [: the carrier of L, the carrier of L:]
[y9,y] is Element of [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric with_suprema RelStr
(L) is Relation-like (L) (L) 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
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, the carrier of L:]
{x,y} is set
{x} is set
{{x,y},{x}} is set
z is Element of the carrier of L
[z,y] is Element of [: the carrier of L, the carrier of L:]
{z,y} is set
{z} is set
{{z,y},{z}} is set
x "\/" z is Element of the carrier of L
[(x "\/" z),y] is Element of [: the carrier of L, the carrier of L:]
{(x "\/" z),y} is set
{(x "\/" z)} is set
{{(x "\/" z),y},{(x "\/" z)}} is set
x "\/" z is Element of the carrier of L
[(x "\/" z),y] is Element of [: the carrier of L, the carrier of L:]
{(x "\/" z),y} is set
{(x "\/" z)} is set
{{(x "\/" z),y},{(x "\/" z)}} is set
L is non empty reflexive transitive antisymmetric lower-bounded /\-complete with_infima RelStr
(L) is Relation-like (L) (L) 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
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, the carrier of L:]
{x,y} is set
{x} is set
{{x,y},{x}} is set
z is Element of the carrier of L
[z,y] is Element of [: the carrier of L, the carrier of L:]
{z,y} is set
{z} is set
{{z,y},{z}} is set
x "\/" z is Element of the carrier of L
[(x "\/" z),y] is Element of [: the carrier of L, the carrier of L:]
{(x "\/" z),y} is set
{(x "\/" z)} is set
{{(x "\/" z),y},{(x "\/" z)}} is set
L is non empty reflexive antisymmetric lower-bounded RelStr
(L) is Relation-like (L) 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
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
R is Element of the carrier of L
[(Bottom L),R] is Element of [: the carrier of L, the carrier of L:]
{(Bottom L),R} is set
{(Bottom L)} is set
{{(Bottom L),R},{(Bottom L)}} is set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
(L) is Relation-like transitive (L) (L) (L) (L) (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
R is Element of the carrier of L
(L,R,(L)) is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,R] in (L) } is set
waybelow R is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 is_way_below R } is set
y9 is set
Y is Element of the carrier of L
[Y,R] is Element of [: the carrier of L, the carrier of L:]
{Y,R} is set
{Y} is set
{{Y,R},{Y}} is set
y9 is set
Y is Element of the carrier of L
[Y,R] is Element of [: the carrier of L, the carrier of L:]
{Y,R} is set
{Y} is set
{{Y,R},{Y}} is set
L is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
(L) is Relation-like (L) (L) (L) 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
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
(L,x,(L)) is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,x] in (L) } is set
"\/" ((L,x,(L)),L) is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : b1 <= x } is set
y9 is set
Y is Element of the carrier of L
[Y,x] is Element of [: the carrier of L, the carrier of L:]
{Y,x} is set
{Y} is set
{{Y,x},{Y}} is set
y9 is set
Y is Element of the carrier of L
[Y,x] is Element of [: the carrier of L, the carrier of L:]
{Y,x} is set
{Y} is set
{{Y,x},{Y}} is set
y9 is set
Y is Element of the carrier of L
y9 is Element of bool the carrier of L
Y is Element of the carrier of L
u is Element of the carrier of L
Y is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous RelStr
(L) is Relation-like transitive (L) (L) (L) (L) (L) 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
R is Element of the carrier of L
(L,R,(L)) is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,R] in (L) } is set
"\/" ((L,R,(L)),L) is Element of the carrier of L
waybelow R is non empty directed lower Element of bool the carrier of L
"\/" ((waybelow R),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous RelStr
(L) is Relation-like transitive (L) (L) (L) (L) (L) 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
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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 Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
R is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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 set
R is set
x is set
x is set
z is set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
(L) is set
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
the Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:] is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
Ids L is non empty set
bool the carrier of L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
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
(L) is non empty strict upper-bounded 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 Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset (L)) is non empty set
[: the carrier of (L), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (L), the carrier of (InclPoset (L)):] is non empty set
R is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
(L) . R is set
x is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
z is Element of the carrier of L
R . z is Element of the carrier of (InclPoset (Ids L))
(L,z,x) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,z] in x } is set
y is set
[y,z] is set
{y,z} is set
{y} is set
{{y,z},{y}} is set
y9 is Element of the carrier of L
Y is Element of the carrier of L
u is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
u . Y is Element of the carrier of (InclPoset (Ids L))
y is set
Y is Element of bool the carrier of L
"\/" (Y,L) is Element of the carrier of L
y9 is Element of the carrier of L
[y9,z] is Element of [: the carrier of L, the carrier of L:]
{y9,z} is set
{y9} is set
{{y9,z},{y9}} is set
"\/" ((L,z,x),L) is Element of the carrier of L
y is Element of bool the carrier of L
"\/" (y,L) is Element of the carrier of L
z is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
Ids L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset (Ids L)) is non empty set
R is Element of the carrier of L
{ ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : verum } is set
meet { ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : verum } is set
waybelow R is non empty directed lower Element of bool the carrier of L
{ ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
downarrow R is non empty directed lower Element of bool the carrier of L
{R} is Element of bool the carrier of L
downarrow {R} is lower Element of bool the carrier of L
{ ((downarrow R) /\ b1) where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
y is set
y9 is non empty directed lower Element of bool the carrier of L
(L,y9) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[: 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
(L,y9) . R is Element of the carrier of (InclPoset (Ids L))
"\/" (y9,L) is Element of the carrier of L
(downarrow R) /\ y9 is Element of bool the carrier of L
y is set
y9 is non empty directed lower Element of bool the carrier of L
(downarrow R) /\ y9 is Element of bool the carrier of L
"\/" (y9,L) is Element of the carrier of L
(L,y9) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[: 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
(L,y9) . R is Element of the carrier of (InclPoset (Ids L))
{ ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : not R <= "\/" (b1,L) } is set
{ (downarrow R) where b1 is non empty directed lower Element of bool the carrier of L : not R <= "\/" (b1,L) } is set
y9 is set
Y is non empty directed lower Element of bool the carrier of L
(L,Y) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[: 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
(L,Y) . R is Element of the carrier of (InclPoset (Ids L))
"\/" (Y,L) is Element of the carrier of L
Y is non empty directed lower Element of bool the carrier of L
(L,Y) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[: 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
(L,Y) . R is Element of the carrier of (InclPoset (Ids L))
"\/" (Y,L) is Element of the carrier of L
y9 is set
Y is non empty directed lower Element of bool the carrier of L
"\/" (Y,L) is Element of the carrier of L
(L,Y) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[: 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
(L,Y) . R is Element of the carrier of (InclPoset (Ids L))
{ ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } \/ { ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : not R <= "\/" (b1,L) } is set
y9 is set
Y is non empty directed lower Element of bool the carrier of L
(L,Y) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[: 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
(L,Y) . R is Element of the carrier of (InclPoset (Ids L))
"\/" (Y,L) is Element of the carrier of L
y9 is set
Y is non empty directed lower Element of bool the carrier of L
(L,Y) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[: 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
(L,Y) . R is Element of the carrier of (InclPoset (Ids L))
"\/" (Y,L) is Element of the carrier of L
u is non empty directed lower Element of bool the carrier of L
(L,u) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
(L,u) . R is Element of the carrier of (InclPoset (Ids L))
"\/" (u,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
y9 is non empty set
the Element of y9 is Element of y9
u is non empty directed lower Element of bool the carrier of L
"\/" (u,L) is Element of the carrier of L
"\/" ((downarrow R),L) is Element of the carrier of L
(downarrow R) /\ (downarrow R) is Element of bool the carrier of L
{ b1 where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
Y is set
y9 is non empty directed lower Element of bool the carrier of L
(downarrow R) /\ y9 is Element of bool the carrier of L
"\/" (y9,L) is Element of the carrier of L
u is non empty directed lower Element of bool the carrier of L
"\/" (u,L) is Element of the carrier of L
meet { b1 where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
meet { ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
Y is non empty directed lower Element of bool the carrier of L
"\/" (Y,L) is Element of the carrier of L
(downarrow R) /\ Y is Element of bool the carrier of L
u is set
y9 is non empty directed lower Element of bool the carrier of L
(downarrow R) /\ y9 is Element of bool the carrier of L
"\/" (y9,L) is Element of the carrier of L
the non empty directed lower Element of bool the carrier of L is non empty directed lower Element of bool the carrier of L
"\/" ( the non empty directed lower Element of bool the carrier of L,L) is Element of the carrier of L
u is set
y9 is non empty directed lower Element of bool the carrier of L
"\/" (y9,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
downarrow (Bottom L) is non empty directed lower Element of bool the carrier of L
{(Bottom L)} is Element of bool the carrier of L
downarrow {(Bottom L)} is lower Element of bool the carrier of L
"\/" ((downarrow (Bottom L)),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
(downarrow R) /\ Y is Element of bool the carrier of L
meet { ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : not R <= "\/" (b1,L) } is set
u is set
y9 is non empty directed lower Element of bool the carrier of L
"\/" (y9,L) is Element of the carrier of L
meet { ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
(meet { ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } ) /\ (meet { ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : not R <= "\/" (b1,L) } ) is set
{ b1 where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
meet { b1 where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
(downarrow R) /\ (meet { b1 where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } ) is Element of bool the carrier of L
u is set
[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L
y9 is Element of bool the carrier of L
"\/" (y9,L) is Element of the carrier of L
y99 is set
Y is non empty directed lower Element of bool the carrier of L
"\/" (Y,L) is Element of the carrier of L
(downarrow R) /\ Y is Element of bool the carrier of L
u is set
y9 is set
y99 is non empty directed lower Element of bool the carrier of L
(downarrow R) /\ y99 is Element of bool the carrier of L
"\/" (y99,L) is Element of the carrier of L
(downarrow R) /\ (waybelow R) is Element of bool the carrier of L
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous 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 set
R is Element of the carrier of L
{ (L,R,b1) where b1 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:] : b1 in (L) } is set
meet { (L,R,b1) where b1 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:] : b1 in (L) } is set
waybelow R is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
the Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:] is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R, the Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,R] in the Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:] } is set
{ b1 where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
meet { b1 where b1 is non empty directed lower Element of bool the carrier of L : R <= "\/" (b1,L) } is set
Ids L is non empty set
{ b1 where b1 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 V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset (Ids L)) is non empty set
{ ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : verum } is set
meet { ((L,b1) . R) where b1 is non empty directed lower Element of bool the carrier of L : verum } is set
the non empty directed lower Element of bool the carrier of L is non empty directed lower Element of bool the carrier of L
(L, the non empty directed lower Element of bool the carrier of L) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
[: 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
(L, the non empty directed lower Element of bool the carrier of L) . R is Element of the carrier of (InclPoset (Ids L))
y9 is set
Y is non empty directed lower Element of bool the carrier of L
(L,Y) is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
(L,Y) . R is Element of the carrier of (InclPoset (Ids L))
(L) is non empty strict upper-bounded RelStr
the carrier of (L) is non empty set
(L) is non empty Relation-like Function-like total quasi_total monotone Element of bool [: the carrier of (L), the carrier of (InclPoset (L)):]
(L) is non empty set
InclPoset (L) is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of (InclPoset (L)) is non empty set
[: the carrier of (L), the carrier of (InclPoset (L)):] is non empty Relation-like set
bool [: the carrier of (L), the carrier of (InclPoset (L)):] is non empty set
(L) . (L,Y) is set
u is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R,u) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,R] in u } is set
y9 is set
[y9,R] is set
{y9,R} is set
{y9} is set
{{y9,R},{y9}} is set
y99 is Element of the carrier of L
Y is Element of the carrier of L
y2 is non empty Relation-like Function-like total quasi_total Element of bool [: the carrier of L, the carrier of (InclPoset (Ids L)):]
y2 . Y is Element of the carrier of (InclPoset (Ids L))
y9 is set
Y is Element of bool the carrier of L
"\/" (Y,L) is Element of the carrier of L
y99 is Element of the carrier of L
[y99,R] is Element of [: the carrier of L, the carrier of L:]
{y99,R} is set
{y99} is set
{{y99,R},{y99}} is set
y9 is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
y9 is set
Y is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R,Y) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,R] in Y } is set
u is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R,u) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,R] in u } is set
"\/" ((L,R,u),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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 Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
z is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
x is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous RelStr
the carrier of x is non empty set
[: the carrier of x, the carrier of x:] is non empty Relation-like set
bool [: the carrier of x, the carrier of x:] is non empty set
y9 is set
Y is set
[y9,Y] is set
{y9,Y} is set
{y9} is set
{{y9,Y},{y9}} is set
u is Element of the carrier of x
y9 is Element of the carrier of x
waybelow y9 is non empty directed lower Element of bool the carrier of x
bool the carrier of x is non empty set
(x) is non empty set
{ (x,y9,b1) where b1 is Relation-like transitive (x) (x) (x) (x) (x) Element of bool [: the carrier of x, the carrier of x:] : b1 in (x) } is set
meet { (x,y9,b1) where b1 is Relation-like transitive (x) (x) (x) (x) (x) Element of bool [: the carrier of x, the carrier of x:] : b1 in (x) } is set
y is Relation-like transitive (x) (x) (x) (x) (x) (x) Element of bool [: the carrier of x, the carrier of x:]
(x,y9,y) is non empty directed lower Element of bool the carrier of x
{ b1 where b1 is Element of the carrier of x : [b1,y9] in y } is set
x is Element of the carrier of L
waybelow x is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
"\/" ((waybelow x),L) is Element of the carrier of L
(L,x,(L)) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,x] in (L) } is set
"\/" ((L,x,(L)),L) is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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 Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
R is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
x is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
z is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
R is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
waybelow x is non empty directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
"\/" ((waybelow x),L) is Element of the carrier of L
(L) is non empty set
{ (L,x,b1) where b1 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:] : b1 in (L) } is set
meet { (L,x,b1) where b1 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:] : b1 in (L) } is set
(L,x,R) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,x] in R } is set
"\/" ((L,x,R),L) is Element of the carrier of L
y is set
y9 is Relation-like transitive (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,x,y9) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,x] in y9 } is set
u is set
Y is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
(L,x,Y) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,x] in Y } is set
L is RelStr
the carrier of L is set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is RelStr
the carrier of L is set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is RelStr
the carrier of L is set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
y is Element of the carrier of L
[x,y] is set
{x,y} is set
{{x,y},{x}} is set
[y,z] is set
{y,z} is set
{y} is set
{{y,z},{y}} is set
y is Element of the carrier of L
[x,y] is set
{x,y} is set
{{x,y},{x}} is set
[y,z] is set
{y,z} is set
{y} is set
{{y,z},{y}} is set
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
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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
R is Element of the carrier of L
x is Element of the carrier of L
z is Relation-like (L) Element of bool [: the carrier of L, the carrier of L:]
(L,R,z) is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,R] in z } is set
"\/" ((L,R,z),L) is Element of the carrier of L
y is Element of the carrier of L
[y,R] is Element of [: the carrier of L, the carrier of L:]
{y,R} is set
{y} is set
{{y,R},{y}} is set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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
R is Element of the carrier of L
x is Element of the carrier of L
[R,x] is Element of [: the carrier of L, the carrier of L:]
{R,x} is set
{R} is set
{{R,x},{R}} is set
z is Relation-like (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
y is Element of the carrier of L
[y,x] is Element of [: the carrier of L, the carrier of L:]
{y,x} is set
{y} is set
{{y,x},{y}} is set
R "\/" y is Element of the carrier of L
y9 is Element of the carrier of L
[y9,x] is Element of [: the carrier of L, the carrier of L:]
{y9,x} is set
{y9} is set
{{y9,x},{y9}} is set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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
R is Element of the carrier of L
x is Element of the carrier of L
z is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
{ b1 where b1 is Element of the carrier of L : ex b2 being Element of the carrier of L st
( [b1,b2] in z & [b2,x] in z ) } is set
Bottom L is Element of the carrier of L
"\/" ({},L) is Element of the carrier of L
[(Bottom L),(Bottom L)] is Element of [: the carrier of L, the carrier of L:]
{(Bottom L),(Bottom L)} is set
{(Bottom L)} is set
{{(Bottom L),(Bottom L)},{(Bottom L)}} is set
[(Bottom L),x] is Element of [: the carrier of L, the carrier of L:]
{(Bottom L),x} is set
{{(Bottom L),x},{(Bottom L)}} is set
y9 is set
Y is Element of the carrier of L
u is Element of the carrier of L
[Y,u] is Element of [: the carrier of L, the carrier of L:]
{Y,u} is set
{Y} is set
{{Y,u},{Y}} is set
[u,x] is Element of [: the carrier of L, the carrier of L:]
{u,x} is set
{u} is set
{{u,x},{u}} is set
bool the carrier of L is non empty set
y9 is non empty Element of bool the carrier of L
Y is Element of the carrier of L
u is Element of the carrier of L
y9 is Element of the carrier of L
y99 is Element of the carrier of L
[y9,y99] is Element of [: the carrier of L, the carrier of L:]
{y9,y99} is set
{y9} is set
{{y9,y99},{y9}} is set
[y99,x] is Element of [: the carrier of L, the carrier of L:]
{y99,x} is set
{y99} is set
{{y99,x},{y99}} is set
y99 is Element of the carrier of L
[y9,y99] is Element of [: the carrier of L, the carrier of L:]
{y9,y99} is set
{y9} is set
{{y9,y99},{y9}} is set
[y99,x] is Element of [: the carrier of L, the carrier of L:]
{y99,x} is set
{y99} is set
{{y99,x},{y99}} is set
[u,y99] is Element of [: the carrier of L, the carrier of L:]
{u,y99} is set
{u} is set
{{u,y99},{u}} is set
Y is Element of the carrier of L
u is Element of the carrier of L
y9 is Element of the carrier of L
y99 is Element of the carrier of L
Y is Element of the carrier of L
[y9,Y] is Element of [: the carrier of L, the carrier of L:]
{y9,Y} is set
{y9} is set
{{y9,Y},{y9}} is set
[Y,x] is Element of [: the carrier of L, the carrier of L:]
{Y,x} is set
{Y} is set
{{Y,x},{Y}} is set
Y is Element of the carrier of L
[y9,Y] is Element of [: the carrier of L, the carrier of L:]
{y9,Y} is set
{y9} is set
{{y9,Y},{y9}} is set
[Y,x] is Element of [: the carrier of L, the carrier of L:]
{Y,x} is set
{Y} is set
{{Y,x},{Y}} is set
y2 is Element of the carrier of L
[y99,y2] is Element of [: the carrier of L, the carrier of L:]
{y99,y2} is set
{y99} is set
{{y99,y2},{y99}} is set
[y2,x] is Element of [: the carrier of L, the carrier of L:]
{y2,x} is set
{y2} is set
{{y2,x},{y2}} is set
y2 is Element of the carrier of L
[y99,y2] is Element of [: the carrier of L, the carrier of L:]
{y99,y2} is set
{y99} is set
{{y99,y2},{y99}} is set
[y2,x] is Element of [: the carrier of L, the carrier of L:]
{y2,x} is set
{y2} is set
{{y2,x},{y2}} is set
Y "\/" u is Element of the carrier of L
Y "\/" y2 is Element of the carrier of L
[(Y "\/" u),(Y "\/" y2)] is Element of [: the carrier of L, the carrier of L:]
{(Y "\/" u),(Y "\/" y2)} is set
{(Y "\/" u)} is set
{{(Y "\/" u),(Y "\/" y2)},{(Y "\/" u)}} is set
[(Y "\/" y2),x] is Element of [: the carrier of L, the carrier of L:]
{(Y "\/" y2),x} is set
{(Y "\/" y2)} is set
{{(Y "\/" y2),x},{(Y "\/" y2)}} is set
Y is non empty directed lower Element of bool the carrier of L
"\/" (Y,L) is Element of the carrier of L
(L,x,z) is non empty directed lower Element of bool the carrier of L
{ b1 where b1 is Element of the carrier of L : [b1,x] in z } is set
y9 is set
y99 is Element of the carrier of L
Y is Element of the carrier of L
[y99,Y] is Element of [: the carrier of L, the carrier of L:]
{y99,Y} is set
{y99} is set
{{y99,Y},{y99}} is set
[Y,x] is Element of [: the carrier of L, the carrier of L:]
{Y,x} is set
{Y} is set
{{Y,x},{Y}} is set
Y is Element of the carrier of L
[y99,Y] is Element of [: the carrier of L, the carrier of L:]
{y99,Y} is set
{y99} is set
{{y99,Y},{y99}} is set
[Y,x] is Element of [: the carrier of L, the carrier of L:]
{Y,x} is set
{Y} is set
{{Y,x},{Y}} is set
[y99,x] is Element of [: the carrier of L, the carrier of L:]
{y99,x} is set
{{y99,x},{y99}} is set
"\/" ((L,x,z),L) is Element of the carrier of L
y9 is Element of the carrier of L
[y9,x] is Element of [: the carrier of L, the carrier of L:]
{y9,x} is set
{y9} is set
{{y9,x},{y9}} is set
y99 is Element of the carrier of L
[y99,y9] is Element of [: the carrier of L, the carrier of L:]
{y99,y9} is set
{y99} is set
{{y99,y9},{y99}} is set
Y is Element of the carrier of L
Y is Element of the carrier of L
u is Element of the carrier of L
y9 is Element of the carrier of L
[u,y9] is Element of [: the carrier of L, the carrier of L:]
{u,y9} is set
{u} is set
{{u,y9},{u}} is set
[y9,x] is Element of [: the carrier of L, the carrier of L:]
{y9,x} is set
{y9} is set
{{y9,x},{y9}} is set
y9 is Element of the carrier of L
[u,y9] is Element of [: the carrier of L, the carrier of L:]
{u,y9} is set
{u} is set
{{u,y9},{u}} is set
[y9,x] is Element of [: the carrier of L, the carrier of L:]
{y9,x} is set
{y9} is set
{{y9,x},{y9}} is set
[R,x] is Element of [: the carrier of L, the carrier of L:]
{R,x} is set
{R} is set
{{R,x},{R}} is set
y99 is Element of the carrier of L
[y99,x] is Element of [: the carrier of L, the carrier of L:]
{y99,x} is set
{y99} is set
{{y99,x},{y99}} is set
y9 "\/" y99 is Element of the carrier of L
[R,(y9 "\/" y99)] is Element of [: the carrier of L, the carrier of L:]
{R,(y9 "\/" y99)} is set
{{R,(y9 "\/" y99)},{R}} is set
[(y9 "\/" y99),x] is Element of [: the carrier of L, the carrier of L:]
{(y9 "\/" y99),x} is set
{(y9 "\/" y99)} is set
{{(y9 "\/" y99),x},{(y9 "\/" y99)}} is set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous RelStr
(L) is Relation-like transitive (L) (L) (L) (L) (L) (L) 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
x is Element of the carrier of L
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
[x,z] is Element of [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous RelStr
(L) is Relation-like transitive (L) (L) (L) (L) (L) (L) 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
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
R is Element of the carrier of L
x is Element of the carrier of L
(L) is Relation-like transitive (L) (L) (L) (L) (L) (L) (L) (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
[R,x] is Element of [: the carrier of L, the carrier of L:]
{R,x} is set
{R} is set
{{R,x},{R}} is set
y is Element of the carrier of L
[R,y] is Element of [: the carrier of L, the carrier of L:]
{R,y} is set
{{R,y},{R}} is set
[y,x] is Element of [: the carrier of L, the carrier of L:]
{y,x} is set
{y} is set
{{y,x},{y}} is set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
R is Element of the carrier of L
x is Element of the carrier of L
z is non empty directed Element of bool the carrier of L
"\/" (z,L) is Element of the carrier of L
y is Element of the carrier of L
y9 is Element of the carrier of L
z is non empty directed Element of bool the carrier of L
"\/" (z,L) is Element of the carrier of L
y is Element of the carrier of L
L is RelStr
the carrier of L is set
bool the carrier of L is non empty set
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
L is RelStr
the carrier of L is set
bool the carrier of L is non empty set
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
R is Element of bool the carrier of L
x is Element of the carrier of L
z is Element of the carrier of L
y is Element of the carrier of L
[x,y] is set
{x,y} is set
{x} is set
{{x,y},{x}} is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
L is RelStr
the carrier of L is set
L is RelStr
the carrier of L is set
R is set
x is Element of the carrier of L
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
z is Element of the carrier of L
z is Element of the carrier of L
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
z is set
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
y is Element of the carrier of L
L is RelStr
the carrier of L is set
L is RelStr
the carrier of L is set
R is set
x is Element of the carrier of L
the InternalRel of L is Relation-like Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
z is Element of the carrier of L
z is Element of the carrier of L
z is Element of the carrier of L
[z,x] is set
{z,x} is set
{z} is set
{{z,x},{z}} is set
z is Element of the carrier of L
[z,x] is set
{z,x} is set
{z} is set
{{z,x},{z}} is set
z is set
[z,x] is set
{z,x} is set
{z} is set
{{z,x},{z}} is set
y is Element of the carrier of L
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
(L,x,R) is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,x] in R } is set
[x,x] is Element of [: the carrier of L, the carrier of L:]
{x,x} is set
{x} is set
{{x,x},{x}} is set
z is Element of the carrier of L
[z,x] is Element of [: the carrier of L, the carrier of L:]
{z,x} is set
{z} is set
{{z,x},{z}} is set
y is Element of the carrier of L
[z,y] is Element of [: the carrier of L, the carrier of L:]
{z,y} is set
{{z,y},{z}} is set
[y,x] is Element of [: the carrier of L, the carrier of L:]
{y,x} is set
{y} is set
{{y,x},{y}} is set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
z is Element of the carrier of L
[x,z] is Element of [: the carrier of L, the carrier of L:]
{x,z} is set
{x} is set
{{x,z},{x}} is set
(L,z,R) is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,z] in R } is set
[z,z] is Element of [: the carrier of L, the carrier of L:]
{z,z} is set
{z} is set
{{z,z},{z}} is set
[z,z] is Element of [: the carrier of L, the carrier of L:]
{z,z} is set
{z} is set
{{z,z},{z}} is set
y is set
[x,y] is set
{x,y} is set
{{x,y},{x}} is set
[y,z] is set
{y,z} is set
{y} is set
{{y,z},{y}} is set
[z,z] is Element of [: the carrier of L, the carrier of L:]
{z,z} is set
{z} is set
{{z,z},{z}} is set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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
R is Relation-like (L) (L) Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
(L,x,R) is directed lower Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,x] in R } is set
z is Element of the carrier of L
y is Element of the carrier of L
[z,x] is Element of [: the carrier of L, the carrier of L:]
{z,x} is set
{z} is set
{{z,x},{z}} is set
[y,x] is Element of [: the carrier of L, the carrier of L:]
{y,x} is set
{y} is set
{{y,x},{y}} is set
y9 is Element of the carrier of L
[z,y9] is Element of [: the carrier of L, the carrier of L:]
{z,y9} is set
{{z,y9},{z}} is set
[y9,x] is Element of [: the carrier of L, the carrier of L:]
{y9,x} is set
{y9} is set
{{y9,x},{y9}} is set
Y is Element of the carrier of L
[y,Y] is Element of [: the carrier of L, the carrier of L:]
{y,Y} is set
{{y,Y},{y}} is set
[Y,x] is Element of [: the carrier of L, the carrier of L:]
{Y,x} is set
{Y} is set
{{Y,x},{Y}} is set
y9 "\/" Y is Element of the carrier of L
u is Element of the carrier of L
[z,u] is set
{z,u} is set
{{z,u},{z}} is set
[y,u] is set
{y,u} is set
{{y,u},{y}} is set
[u,x] is Element of [: the carrier of L, the carrier of L:]
{u,x} is set
{u} is set
{{u,x},{u}} is set
[z,u] is Element of [: the carrier of L, the carrier of L:]
[y,u] is Element of [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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
R is Relation-like Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
[x,z] is Element of [: the carrier of L, the carrier of L:]
(L,z,R) is Element of bool the carrier of L
bool the carrier of L is non empty set
{ b1 where b1 is Element of the carrier of L : [b1,z] in R } is set
y is Element of the carrier of L
[x,y] is Element of [: the carrier of L, the carrier of L:]
{x,y} is set
{{x,y},{x}} is set
[x,y] is set
[y,z] is set
{y,z} is set
{y} is set
{{y,z},{y}} is set
[y,z] is Element of [: the carrier of L, the carrier of L:]
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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
R is Relation-like transitive (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]
x is Element of the carrier of L
z is Element of the carrier of L
[x,z] is set
{x,z} is set
{x} is set
{{x,z},{x}} is set
[x,z] is Element of [: the carrier of L, the carrier of L:]
y is Element of the carrier of L
[x,y] is Element of [: the carrier of L, the carrier of L:]
{x,y} is set
{{x,y},{x}} is set
[y,z] is Element of [: the carrier of L, the carrier of L:]
{y,z} is set
{y} is set
{{y,z},{y}} is set
y9 is Element of the carrier of L
[y9,z] is Element of [: the carrier of L, the carrier of L:]
{y9,z} is set
{y9} is set
{{y9,z},{y9}} is set
y "\/" y9 is Element of the carrier of L
Y is Element of the carrier of L
[x,Y] is set
{x,Y} is set
{{x,Y},{x}} is set
[Y,z] is set
{Y,z} is set
{Y} is set
{{Y,z},{Y}} is set
L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V152() up-complete /\-complete with_suprema with_infima complete 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
R is Relation-like transitive (L) (L) (L) (L) (L) (L) Element of bool [: the carrier of L, the carrier of L:]