:: WAYBEL_4 semantic presentation

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

[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

{ b

[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

{ b

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

{ b

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

{ b

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

c

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

c

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

c

the carrier of c

c

c

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

{ b

(L,z,R) is lower Element of bool the carrier of L

{ b

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

{ b

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

{ b

(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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

(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

{ b

( b

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

{ b

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

{ b

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