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