:: LATTICE7 semantic presentation

REAL is V32() V33() V34() V38() set
NAT is V32() V33() V34() V35() V36() V37() V38() Element of bool REAL
bool REAL is non empty set
NAT is V32() V33() V34() V35() V36() V37() V38() set
bool NAT is non empty set
bool NAT is non empty set
{} is empty V32() V33() V34() V35() V36() V37() V38() set
1 is non empty V23() V24() ext-real positive non negative V32() V33() V34() V35() V36() V37() Element of NAT
2 is non empty V23() V24() ext-real positive non negative V32() V33() V34() V35() V36() V37() Element of NAT
L is 1-sorted
the carrier of L is set
bool the carrier of L is non empty set
X is Element of bool the carrier of L
f is Element of bool the carrier of L
b is set
b is Element of the carrier of L
Z1 is Element of the carrier of L

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
{()} is non empty Element of bool the carrier of L

the carrier of L is non empty set
X is Element of the carrier of L
f is Element of the carrier of L
bool the carrier of L is non empty set
{X,f} is non empty Element of bool the carrier of L
b is non empty strongly_connected Element of bool the carrier of L
Z1 is Element of the carrier of L

the carrier of L is non empty set
X is Element of the carrier of L
f is Element of the carrier of L
{X,f} is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
b is Element of the carrier of L

the carrier of L is non empty V43() set
Bottom L is Element of the carrier of L
X is Element of the carrier of L
{(),X} is non empty V43() Element of bool the carrier of L
bool the carrier of L is non empty set
card {(),X} is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is non empty V43() strongly_connected (L, Bottom L,X)
card f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
card the carrier of L is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is V23() ext-real set
b is non empty V43() strongly_connected (L, Bottom L,X)
card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is V23() ext-real set
b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Z is non empty V43() strongly_connected (L, Bottom L,X)
card Z is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
r2 is non empty V43() strongly_connected (L, Bottom L,X)
card r2 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is non empty V43() strongly_connected (L, Bottom L,X)
card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is non empty V43() strongly_connected (L, Bottom L,X)
card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Z1 is non empty V43() strongly_connected (L, Bottom L,X)
card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Z1 is non empty V43() strongly_connected (L, Bottom L,X)
card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Z is non empty V43() strongly_connected (L, Bottom L,X)
card Z is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

the carrier of L is non empty V43() set
X is Element of the carrier of L
f is Element of the carrier of L
(L,f) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
(L,X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Bottom L is Element of the carrier of L
b is non empty V43() strongly_connected (L, Bottom L,X)
card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is non empty V43() strongly_connected (L, Bottom L,X)
card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is non empty V43() strongly_connected (L, Bottom L,X)
card b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
{f} is non empty V43() Element of bool the carrier of L
bool the carrier of L is non empty set
b \/ {f} is non empty V43() Element of bool the carrier of L
card (b \/ {f}) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
(card b) + 1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
the InternalRel of L is V7() V10( the carrier of L) V11( the carrier of L) V28( the carrier of L) reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
Z is set
r2 is set
[Z,r2] is set
{Z,r2} is non empty set
{Z} is non empty set
{{Z,r2},{Z}} is non empty set
[r2,Z] is set
{r2,Z} is non empty set
{r2} is non empty set
{{r2,Z},{r2}} is non empty set
y is Element of the carrier of L
a is Element of the carrier of L
y is Element of the carrier of L
y is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
Z is Element of the carrier of L
(L,X) + 1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

the carrier of L is non empty V43() set
bool the carrier of L is non empty set
X is V43() strongly_connected Element of bool the carrier of L
f is Element of the carrier of L
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
(L,f) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

the carrier of L is non empty V43() set
bool the carrier of L is non empty set
X is V43() strongly_connected Element of bool the carrier of L
f is Element of the carrier of L
b is Element of the carrier of L
(L,f) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

the carrier of L is non empty V43() set
bool the carrier of L is non empty set
X is V43() strongly_connected Element of bool the carrier of L
f is Element of the carrier of L
b is Element of the carrier of L
(L,f) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

the carrier of L is non empty V43() set
Bottom L is Element of the carrier of L
X is Element of the carrier of L
(L,X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
{()} is non empty V43() Element of bool the carrier of L
bool the carrier of L is non empty set
f is non empty V43() strongly_connected (L, Bottom L, Bottom L)
b is set
Z1 is Element of f
b is set
(L,()) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
card {()} is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is non empty V43() strongly_connected (L, Bottom L, Bottom L)
card f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
{(),X} is non empty V43() Element of bool the carrier of L
bool the carrier of L is non empty set
f is Element of the carrier of L
card {(),X} is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

the carrier of L is non empty V43() set
X is Element of the carrier of L
(L,X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Bottom L is Element of the carrier of L
{(),X} is non empty V43() Element of bool the carrier of L
bool the carrier of L is non empty set
card {(),X} is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
{()} is non empty V43() Element of bool the carrier of L
{(),()} is non empty V43() Element of bool the carrier of L
f is Element of the carrier of L
f is Element of the carrier of L
card {(),()} is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
(L,()) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

the carrier of F1() is non empty V43() set
L is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
L + 1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
X is Element of the carrier of F1()
(F1(),X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is Element of the carrier of F1()
(F1(),f) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
X is Element of the carrier of F1()
(F1(),X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
L is Element of the carrier of F1()
X is Element of the carrier of F1()
X is Element of the carrier of F1()
(F1(),X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
0 is empty V23() V24() ext-real non positive non negative V32() V33() V34() V35() V36() V37() V38() Element of NAT
X is Element of the carrier of F1()
(F1(),X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
X is Element of the carrier of F1()
(F1(),X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
is non empty set
is non empty set
bool is non empty set

the carrier of L is non empty set

the carrier of L is non empty V43() set
bool the carrier of L is non empty set
X is non empty V43() Element of bool the carrier of L
card the carrier of L is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is V23() ext-real set
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Bottom L is Element of the carrier of L
Z1 is non empty V43() strongly_connected (L, Bottom L,b)
card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is set
Bottom L is Element of the carrier of L
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Z1 is non empty V43() strongly_connected (L, Bottom L,b)
card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is V23() ext-real set
Z1 is Element of the carrier of L
b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
(L,Z1) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is Element of the carrier of L
f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Z1 is Element of the carrier of L
(L,Z1) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

the carrier of L is non empty V43() set
bool the carrier of L is non empty set
X is non empty V43() strongly_connected Element of bool the carrier of L
card the carrier of L is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is V23() ext-real set
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Bottom L is Element of the carrier of L
Z1 is non empty V43() strongly_connected (L, Bottom L,b)
card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is set
Bottom L is Element of the carrier of L
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Z1 is non empty V43() strongly_connected (L, Bottom L,b)
card Z1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is V23() ext-real set
Z1 is Element of the carrier of L
b is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
(L,Z1) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is Element of the carrier of L
f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
b is Element of the carrier of L
(L,b) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
Z1 is Element of the carrier of L
(L,Z1) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is Element of the carrier of L
b is Element of the carrier of L

the carrier of L is non empty V43() set
Bottom L is Element of the carrier of L
X is Element of the carrier of L
(L,X) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is non empty V43() strongly_connected (L, Bottom L,X)
card f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is non empty V43() strongly_connected (L, Bottom L,X)
card f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
f is non empty V43() strongly_connected (L, Bottom L,X)
card f is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
{X} is non empty V43() Element of bool the carrier of L
bool the carrier of L is non empty set
f \ {X} is V43() Element of bool the carrier of L
the InternalRel of L is V7() V10( the carrier of L) V11( the carrier of L) V28( the carrier of L) reflexive antisymmetric transitive Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
Z1 is set
Z is set
[Z1,Z] is set
{Z1,Z} is non empty set
{Z1} is non empty set
{{Z1,Z},{Z1}} is non empty set
[Z,Z1] is set
{Z,Z1} is non empty set
{Z} is non empty set
{{Z,Z1},{Z}} is non empty set
r2 is Element of the carrier of L
y is Element of the carrier of L
Z1 is non empty V43() strongly_connected Element of bool the carrier of L
(L,Z1) is Element of the carrier of L
Z is Element of the carrier of L
r2 is Element of the carrier of L
{r2} is non empty V43() Element of bool the carrier of L
f \/ {r2} is non empty V43() Element of bool the carrier of L
a is Element of the carrier of L
(f \ {X}) \/ {X} is non empty V43() Element of bool the carrier of L
a is set
A is set
[a,A] is set
{a,A} is non empty set
{a} is non empty set
{{a,A},{a}} is non empty set
[A,a] is set
{A,a} is non empty set
{A} is non empty set
{{A,a},{A}} is non empty set
y is Element of the carrier of L
a is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
y is Element of the carrier of L
y is Element of the carrier of L
a is Element of the carrier of L
a is Element of the carrier of L
card (f \/ {r2}) is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT
(card f) + 1 is V23() V24() ext-real V32() V33() V34() V35() V36() V37() Element of NAT

the carrier of L is non empty set
Bottom L is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( not b1 = Bottom L & ( for b2, b3 being Element of the carrier of L holds
( not b1 = b2 "\/" b3 or b1 = b2 or b1 = b3 ) ) )
}
is set

bool the carrier of L is non empty set
X is set
f is Element of the carrier of L

the carrier of L is non empty set
(L) is Element of bool the carrier of L
bool the carrier of L is non empty set
Bottom L is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( not b1 = Bottom L & ( for b2, b3 being Element of the carrier of L holds
( not b1 = b2 "\/" b3 or b1 = b2 or b1 = b3 ) ) )
}
is set

X is Element of the carrier of L
f is Element of the carrier of L
b is Element of the carrier of L
f "\/" b is Element of the carrier of L
Z1 is Element of the carrier of L

the carrier of L is non empty V43() set
(L) is V43() Element of bool the carrier of L
bool the carrier of L is non empty set
Bottom L is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( not b1 = Bottom L & ( for b2, b3 being Element of the carrier of L holds
( not b1 = b2 "\/" b3 or b1 = b2 or b1 = b3 ) ) )
}
is set

X is Element of the carrier of L
f is Element of the carrier of L
b is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 < X & not b1 <= f ) } is set
Z1 is set
Z is set
r2 is Element of the carrier of L
Z is Element of the carrier of L
r2 is Element of the carrier of L
y is Element of the carrier of L
Z "\/" f is Element of the carrier of L
Z "/\" Z is Element of the carrier of L
f "/\" f is Element of the carrier of L

the carrier of L is non empty V43() set
(L) is V43() Element of bool the carrier of L
bool the carrier of L is non empty set
Bottom L is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( not b1 = Bottom L & ( for b2, b3 being Element of the carrier of L holds
( not b1 = b2 "\/" b3 or b1 = b2 or b1 = b3 ) ) )
}
is set

X is Element of the carrier of L
downarrow X is V43() Element of bool the carrier of L
{X} is non empty V43() Element of bool the carrier of L
downarrow {X} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
"\/" ((() /\ (L)),L) is Element of the carrier of L
{()} is non empty V43() Element of bool the carrier of L
{()} /\ (L) is V43() Element of bool the carrier of L
the Element of {()} /\ (L) is Element of {()} /\ (L)
f is Element of the carrier of L
b is Element of the carrier of L
f "\/" b is Element of the carrier of L
downarrow f is V43() Element of bool the carrier of L
{f} is non empty V43() Element of bool the carrier of L
downarrow {f} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
downarrow b is V43() Element of bool the carrier of L
{b} is non empty V43() Element of bool the carrier of L
downarrow {b} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
(() /\ (L)) \/ (() /\ (L)) is V43() Element of bool the carrier of L
Z1 is Element of the carrier of L
Z1 "/\" X is Element of the carrier of L
Z1 "/\" f is Element of the carrier of L
Z1 "/\" b is Element of the carrier of L
(Z1 "/\" f) "\/" (Z1 "/\" b) is Element of the carrier of L
Z1 is Element of the carrier of L
"\/" ((() /\ (L)),L) is Element of the carrier of L
"\/" ((() /\ (L)),L) is Element of the carrier of L
("\/" ((() /\ (L)),L)) "\/" ("\/" ((() /\ (L)),L)) is Element of the carrier of L
f "\/" ("\/" ((() /\ (L)),L)) is Element of the carrier of L
"\/" ((),L) is Element of the carrier of L

the carrier of L is non empty V43() set
(L) is V43() Element of bool the carrier of L
bool the carrier of L is non empty set
Bottom L is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( not b1 = Bottom L & ( for b2, b3 being Element of the carrier of L holds
( not b1 = b2 "\/" b3 or b1 = b2 or b1 = b3 ) ) )
}
is set

X is Element of the carrier of L
downarrow X is V43() Element of bool the carrier of L
{X} is non empty V43() Element of bool the carrier of L
downarrow {X} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
"\/" ((() /\ (L)),L) is Element of the carrier of L
f is Element of the carrier of L
downarrow f is V43() Element of bool the carrier of L
{f} is non empty V43() Element of bool the carrier of L
downarrow {f} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
"\/" ((() /\ (L)),L) is Element of the carrier of L
"\/" ((),L) is Element of the carrier of L
L is RelStr
the carrier of L is set
bool the carrier of L is non empty set
{ b1 where b1 is Element of bool the carrier of L : b1 is lower } is set
{} L is empty V32() V33() V34() V35() V36() V37() V38() strongly_connected lower upper Element of bool the carrier of L

the carrier of L is non empty V43() set
(L) is V43() Element of bool the carrier of L
bool the carrier of L is non empty set
Bottom L is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( not b1 = Bottom L & ( for b2, b3 being Element of the carrier of L holds
( not b1 = b2 "\/" b3 or b1 = b2 or b1 = b3 ) ) )
}
is set

((subrelstr (L))) is non empty set
the carrier of (subrelstr (L)) is set
bool the carrier of (subrelstr (L)) is non empty set
{ b1 where b1 is Element of bool the carrier of (subrelstr (L)) : b1 is lower } is set
InclPoset ((subrelstr (L))) is non empty strict V117() reflexive transitive antisymmetric RelStr
the carrier of (InclPoset ((subrelstr (L)))) is non empty set
[: the carrier of L, the carrier of (InclPoset ((subrelstr (L)))):] is non empty set
bool [: the carrier of L, the carrier of (InclPoset ((subrelstr (L)))):] is non empty set
f is V7() V10( the carrier of L) Function-like V28( the carrier of L) set
rng f is set
b is set
dom f is V43() Element of bool the carrier of L
Z1 is set
f . Z1 is set
Z is Element of the carrier of L
downarrow Z is V43() Element of bool the carrier of L
{Z} is non empty V43() Element of bool the carrier of L
downarrow {Z} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
r2 is Element of bool the carrier of (subrelstr (L))
y is Element of the carrier of (subrelstr (L))
a is Element of the carrier of (subrelstr (L))
A is Element of the carrier of L
y is Element of the carrier of L
dom f is V43() Element of bool the carrier of L
b is V7() V10( the carrier of L) V11( the carrier of (InclPoset ((subrelstr (L))))) Function-like V29( the carrier of L, the carrier of (InclPoset ((subrelstr (L))))) Element of bool [: the carrier of L, the carrier of (InclPoset ((subrelstr (L)))):]
Z1 is Element of the carrier of L
Z is Element of the carrier of L
b . Z1 is Element of the carrier of (InclPoset ((subrelstr (L))))
b . Z is Element of the carrier of (InclPoset ((subrelstr (L))))
downarrow Z1 is V43() Element of bool the carrier of L
{Z1} is non empty V43() Element of bool the carrier of L
downarrow {Z1} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
downarrow Z is V43() Element of bool the carrier of L
{Z} is non empty V43() Element of bool the carrier of L
downarrow {Z} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
r2 is Element of the carrier of L
downarrow Z1 is V43() Element of bool the carrier of L
{Z1} is non empty V43() Element of bool the carrier of L
downarrow {Z1} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
downarrow Z is V43() Element of bool the carrier of L
{Z} is non empty V43() Element of bool the carrier of L
downarrow {Z} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
r2 is V43() Element of bool the carrier of L
y is V43() Element of bool the carrier of L
"\/" (r2,L) is Element of the carrier of L
"\/" (y,L) is Element of the carrier of L
"\/" ((() /\ (L)),L) is Element of the carrier of L
"\/" ((() /\ (L)),L) is Element of the carrier of L
rng b is Element of bool the carrier of (InclPoset ((subrelstr (L))))
bool the carrier of (InclPoset ((subrelstr (L)))) is non empty set
Z1 is set
Z is Element of bool the carrier of (subrelstr (L))
dom b is V43() Element of bool the carrier of L
r2 is V43() Element of bool the carrier of L
"\/" (r2,L) is Element of the carrier of L
y is Element of the carrier of L
b . y is set
downarrow ("\/" (r2,L)) is V43() Element of bool the carrier of L
{("\/" (r2,L))} is non empty V43() Element of bool the carrier of L
downarrow {("\/" (r2,L))} is V43() Element of bool the carrier of L
(downarrow ("\/" (r2,L))) /\ (L) is V43() Element of bool the carrier of L
a is Element of the carrier of L
A is Element of the carrier of L
y is Element of the carrier of L
{A} is non empty V43() Element of bool the carrier of L
{A} "/\" r2 is V43() Element of bool the carrier of L
a is Element of the carrier of L
{ (A "/\" b1) where b1 is Element of the carrier of L : b1 in r2 } is set
x is Element of the carrier of L
A "/\" x is Element of the carrier of L
{A,x} is non empty V43() Element of bool the carrier of L
r9 is Element of the carrier of (subrelstr (L))
x9 is Element of the carrier of (subrelstr (L))
"\/" (({A} "/\" r2),L) is Element of the carrier of L
A "/\" ("\/" (r2,L)) is Element of the carrier of L
a is Element of the carrier of L
y is Element of the carrier of L
y is Element of the carrier of L
bool (L) is non empty set
b . y is Element of the carrier of (InclPoset ((subrelstr (L))))
y is set
b . y is set
Z1 is Element of the carrier of L
b . Z1 is Element of the carrier of (InclPoset ((subrelstr (L))))
Z is Element of the carrier of L
b . Z is Element of the carrier of (InclPoset ((subrelstr (L))))
downarrow Z is V43() Element of bool the carrier of L
{Z} is non empty V43() Element of bool the carrier of L
downarrow {Z} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
downarrow Z1 is V43() Element of bool the carrier of L
{Z1} is non empty V43() Element of bool the carrier of L
downarrow {Z1} is V43() Element of bool the carrier of L
() /\ (L) is V43() Element of bool the carrier of L
"\/" ((() /\ (L)),L) is Element of the carrier of L
r2 is V43() Element of bool the carrier of L
"\/" (r2,L) is Element of the carrier of L
"\/" ((() /\ (L)),L) is Element of the carrier of L

(L) is V43() Element of bool the carrier of L
the carrier of L is non empty V43() set
bool the carrier of L is non empty set
Bottom L is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( not b1 = Bottom L & ( for b2, b3 being Element of the carrier of L holds
( not b1 = b2 "\/" b3 or b1 = b2 or b1 = b3 ) ) )
}
is set

((subrelstr (L))) is non empty set
the carrier of (subrelstr (L)) is set
bool the carrier of (subrelstr (L)) is non empty set
{ b1 where b1 is Element of bool the carrier of (subrelstr (L)) : b1 is lower } is set
InclPoset ((subrelstr (L))) is non empty strict V117() reflexive transitive antisymmetric RelStr
the carrier of (InclPoset ((subrelstr (L)))) is non empty set
[: the carrier of L, the carrier of (InclPoset ((subrelstr (L)))):] is non empty set
bool [: the carrier of L, the carrier of (InclPoset ((subrelstr (L)))):] is non empty set
X is V7() V10( the carrier of L) V11( the carrier of (InclPoset ((subrelstr (L))))) Function-like V29( the carrier of L, the carrier of (InclPoset ((subrelstr (L))))) Element of bool [: the carrier of L, the carrier of (InclPoset ((subrelstr (L)))):]
the set is set
bool the set is non empty set
X is non empty set
f is set
b is set
f /\ b is set
f \/ b is set
is non empty set
L is non empty set
X is set
f is set
X /\ f is set
X \/ f is set
L is non empty RelStr
the carrier of L is non empty set
X is non empty RelStr
the carrier of X is non empty set
[: the carrier of L, the carrier of X:] is non empty set
bool [: the carrier of L, the carrier of X:] is non empty set
f is V7() V10( the carrier of L) V11( the carrier of X) Function-like V29( the carrier of L, the carrier of X) Element of bool [: the carrier of L, the carrier of X:]
b is Element of the carrier of L
Z1 is Element of the carrier of L
{b,Z1} is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
L is non empty RelStr
the carrier of L is non empty set
X is non empty RelStr
the carrier of X is non empty set
[: the carrier of L, the carrier of X:] is non empty set
bool [: the carrier of L, the carrier of X:] is non empty set
f is V7() V10( the carrier of L) V11( the carrier of X) Function-like V29( the carrier of L, the carrier of X) Element of bool [: the carrier of L, the carrier of X:]
b is Element of the carrier of L
Z1 is Element of the carrier of L
{b,Z1} is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
L is non empty ()

the carrier of () is non empty set
X is Element of the carrier of ()
f is Element of the carrier of ()
b is Element of the carrier of ()
f "\/" b is Element of the carrier of ()
X "/\" (f "\/" b) is Element of the carrier of ()
X "/\" f is Element of the carrier of ()
X "/\" b is Element of the carrier of ()
(X "/\" f) "\/" (X "/\" b) is Element of the carrier of ()
X /\ b is set
f \/ b is set
X /\ f is set
Z is Element of the carrier of ()
Z1 is Element of the carrier of ()
X /\ Z1 is set
X "/\" Z1 is Element of the carrier of ()
X /\ (f \/ b) is set
(X /\ f) \/ (X /\ b) is set
r2 is Element of the carrier of ()
Z \/ r2 is set
X is set
f is set
X /\ f is set
b is set
Z1 is set
b \/ Z1 is set

(L) is V43() Element of bool the carrier of L
the carrier of L is non empty V43() set
bool the carrier of L is non empty set
Bottom L is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( not b1 = Bottom L & ( for b2, b3 being Element of the carrier of L holds
( not b1 = b2 "\/" b3 or b1 = b2 or b1 = b3 ) ) )
}
is set

((subrelstr (L))) is non empty set
the carrier of (subrelstr (L)) is set
bool the carrier of (subrelstr (L)) is non empty set
{ b1 where b1 is Element of bool the carrier of (subrelstr (L)) : b1 is lower } is set
f is set
b is set
f /\ b is set
f \/ b is set
Z1 is Element of bool the carrier of (subrelstr (L))
Z is Element of bool the carrier of (subrelstr (L))
Z \/ Z1 is Element of bool the carrier of (subrelstr (L))
Z1 is Element of bool the carrier of (subrelstr (L))
Z is Element of bool the carrier of (subrelstr (L))
Z /\ Z1 is Element of bool the carrier of (subrelstr (L))

(L) is V43() Element of bool the carrier of L
the carrier of L is non empty V43() set
bool the carrier of L is non empty set
Bottom L is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( not b1 = Bottom L & ( for b2, b3 being Element of the carrier of L holds
( not b1 = b2 "\/" b3 or b1 = b2 or b1 = b3 ) ) )
}
is set

((subrelstr (L))) is non empty set
the carrier of (subrelstr (L)) is set
bool the carrier of (subrelstr (L)) is non empty set
{ b1 where b1 is Element of bool the carrier of (subrelstr (L)) : b1 is lower } is set
X is set

X is non empty ()

the carrier of L is non empty V43() set
the carrier of () is non empty set
[: the carrier of L, the carrier of ():] is non empty set
bool [: the carrier of L, the carrier of ():] is non empty set
f is V7() V10( the carrier of L) V11( the carrier of ()) Function-like V29( the carrier of L, the carrier of ()) Element of bool [: the carrier of L, the carrier of ():]