:: LATTICE8 semantic presentation

REAL is set
NAT is epsilon-transitive epsilon-connected ordinal non empty V40() V45() V46() Element of bool REAL
bool REAL is non empty set
NAT is epsilon-transitive epsilon-connected ordinal non empty V40() V45() V46() set
bool NAT is non empty V40() V271() set
COMPLEX is set
RAT is set
INT is set
bool NAT is non empty V40() V271() set
{} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty trivial V33() V34() ext-real V38() V40() V45() V47( {} ) FinSequence-membered set
the epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty trivial V33() V34() ext-real V38() V40() V45() V47( {} ) FinSequence-membered set is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty trivial V33() V34() ext-real V38() V40() V45() V47( {} ) FinSequence-membered set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real positive V38() V40() V45() Element of NAT
{{},1} is non empty set
2 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real positive V38() V40() V45() Element of NAT
[:2,2:] is non empty set
[:[:2,2:],2:] is non empty set
bool [:[:2,2:],2:] is non empty V271() set
3 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real positive V38() V40() V45() Element of NAT
0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty trivial V33() V34() ext-real V38() V40() V45() V47( {} ) FinSequence-membered Element of NAT
4 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real positive V38() V40() V45() Element of NAT
the non empty finite reflexive transitive antisymmetric lower-bounded upper-bounded V227() distributive with_suprema with_infima V297() modular RelStr is non empty finite reflexive transitive antisymmetric lower-bounded upper-bounded V227() distributive with_suprema with_infima V297() modular RelStr
2 * 0 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() even Element of NAT
(2 * 0) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() non even Element of NAT
2 * 1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() even Element of NAT
L is non empty non trivial set
EqRelLATT L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V227() with_suprema with_infima V297() RelStr
the carrier of (EqRelLATT L) is non empty set
nabla L is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
[:L,L:] is non empty set
bool [:L,L:] is non empty V271() set
id L is Relation-like L -defined L -valued Function-like one-to-one non empty total V72() V74() V75() V79() Element of bool [:L,L:]
the Element of L is Element of L
{ the Element of L} is non empty trivial V47(1) Element of bool L
bool L is non empty V271() set
L \ { the Element of L} is non empty Element of bool L
the Element of L \ { the Element of L} is Element of L \ { the Element of L}
A is Element of the carrier of (EqRelLATT L)
D is Element of the carrier of (EqRelLATT L)
{A,D} is non empty Element of bool the carrier of (EqRelLATT L)
bool the carrier of (EqRelLATT L) is non empty V271() set
subrelstr {A,D} is non empty strict reflexive transitive antisymmetric full SubRelStr of EqRelLATT L
the carrier of (subrelstr {A,D}) is non empty set
FD is Element of the carrier of (EqRelLATT L)
f is Element of the carrier of (EqRelLATT L)
{FD,f} is non empty Element of bool the carrier of (EqRelLATT L)
"/\" ({FD,f},(EqRelLATT L)) is Element of the carrier of (EqRelLATT L)
A "/\" A is Element of the carrier of (EqRelLATT L)
A "/\" D is Element of the carrier of (EqRelLATT L)
D "/\" A is Element of the carrier of (EqRelLATT L)
D "/\" D is Element of the carrier of (EqRelLATT L)
FD is set
FD is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real positive V38() V40() V45() Element of NAT
f is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
FS is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
f "\/" FS is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
f is set
FD is set
[f,FD] is non empty V25() set
{f,FD} is non empty set
{f} is non empty trivial V47(1) set
{{f,FD},{f}} is non empty set
A9 is set
d9 is set
Aq9 is set
[d9,Aq9] is non empty V25() set
{d9,Aq9} is non empty set
{d9} is non empty trivial V47(1) set
{{d9,Aq9},{d9}} is non empty set
<*f,A9,FD*> is Relation-like NAT -defined Function-like non empty V40() V47(3) FinSequence-like FinSubsequence-like set
d9 is Relation-like NAT -defined L -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of L
len d9 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() Element of NAT
d9 . 2 is set
d9 . 1 is set
Aq9 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
d9 . Aq9 is set
Aq9 + 1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
d9 . (Aq9 + 1) is set
[(d9 . Aq9),(d9 . (Aq9 + 1))] is non empty V25() set
{(d9 . Aq9),(d9 . (Aq9 + 1))} is non empty set
{(d9 . Aq9)} is non empty trivial V47(1) set
{{(d9 . Aq9),(d9 . (Aq9 + 1))},{(d9 . Aq9)}} is non empty set
2 + 1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
dq9 is set
q is set
[dq9,q] is non empty V25() set
{dq9,q} is non empty set
{dq9} is non empty trivial V47(1) set
{{dq9,q},{dq9}} is non empty set
dq9 is set
q is set
[dq9,q] is non empty V25() set
{dq9,q} is non empty set
{dq9} is non empty trivial V47(1) set
{{dq9,q},{dq9}} is non empty set
D "\/" A is Element of the carrier of (EqRelLATT L)
d9 . 3 is set
d9 . 2 is set
d9 . 3 is set
Aq9 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
d9 . Aq9 is set
Aq9 + 1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
d9 . (Aq9 + 1) is set
[(d9 . Aq9),(d9 . (Aq9 + 1))] is non empty V25() set
{(d9 . Aq9),(d9 . (Aq9 + 1))} is non empty set
{(d9 . Aq9)} is non empty trivial V47(1) set
{{(d9 . Aq9),(d9 . (Aq9 + 1))},{(d9 . Aq9)}} is non empty set
2 + 1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
A "\/" D is Element of the carrier of (EqRelLATT L)
dq9 is set
q is set
[dq9,q] is non empty V25() set
{dq9,q} is non empty set
{dq9} is non empty trivial V47(1) set
{{dq9,q},{dq9}} is non empty set
dq9 is set
q is set
[dq9,q] is non empty V25() set
{dq9,q} is non empty set
{dq9} is non empty trivial V47(1) set
{{dq9,q},{dq9}} is non empty set
d9 . 1 is set
FD is Element of the carrier of (EqRelLATT L)
f is Element of the carrier of (EqRelLATT L)
{FD,f} is non empty Element of bool the carrier of (EqRelLATT L)
"\/" ({FD,f},(EqRelLATT L)) is Element of the carrier of (EqRelLATT L)
A "\/" A is Element of the carrier of (EqRelLATT L)
A "\/" D is Element of the carrier of (EqRelLATT L)
D "\/" A is Element of the carrier of (EqRelLATT L)
D "\/" D is Element of the carrier of (EqRelLATT L)
FD is Element of the carrier of (subrelstr {A,D})
{FD} is non empty trivial V47(1) Element of bool the carrier of (subrelstr {A,D})
bool the carrier of (subrelstr {A,D}) is non empty V271() set
[ the Element of L, the Element of L \ { the Element of L}] is non empty V25() Element of [:L,(L \ { the Element of L}):]
[:L,(L \ { the Element of L}):] is non empty set
{ the Element of L, the Element of L \ { the Element of L}} is non empty set
{ the Element of L} is non empty trivial V47(1) set
{{ the Element of L, the Element of L \ { the Element of L}},{ the Element of L}} is non empty set
FD is non empty reflexive transitive antisymmetric full meet-inheriting join-inheriting with_suprema with_infima SubRelStr of EqRelLATT L
succ {} is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() set
L is non empty set
[:L,L:] is non empty set
A is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
the carrier of A is non empty set
[:[:L,L:], the carrier of A:] is non empty set
bool [:[:L,L:], the carrier of A:] is non empty V271() set
D is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total symmetric zeroed u.t.i. Element of bool [:[:L,L:], the carrier of A:]
DistEsti D is epsilon-transitive epsilon-connected ordinal V45() set
L is non empty trivial finite 1 -element reflexive transitive antisymmetric lower-bounded upper-bounded V227() with_suprema with_infima V297() RelStr
the carrier of L is non empty trivial V40() V47(1) set
A is Element of the carrier of L
S is Element of the carrier of L
D is Element of the carrier of L
D "/\" S is Element of the carrier of L
A "\/" (D "/\" S) is Element of the carrier of L
A "\/" D is Element of the carrier of L
(A "\/" D) "/\" S is Element of the carrier of L
D "/\" S is Element of the carrier of L
A "\/" (D "/\" S) is Element of the carrier of L
A "\/" D is Element of the carrier of L
(A "\/" D) "/\" S is Element of the carrier of L
L is non empty set
EqRelLATT L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V227() with_suprema with_infima V297() RelStr
[:L,L:] is non empty set
bool [:L,L:] is non empty V271() set
id L is Relation-like L -defined L -valued Function-like one-to-one non empty total V72() V74() V75() V79() Element of bool [:L,L:]
A is non empty meet-inheriting join-inheriting SubRelStr of EqRelLATT L
the carrier of A is non empty set
D is set
the carrier of (EqRelLATT L) is non empty set
{D} is non empty trivial V47(1) set
FS is set
FS is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
S is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
FS is set
D is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
the carrier of L is non empty set
A is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
the carrier of A is non empty set
[: the carrier of L, the carrier of A:] is non empty set
bool [: the carrier of L, the carrier of A:] is non empty V271() set
D is Relation-like the carrier of L -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of L, the carrier of A:]
S is Element of the carrier of L
FS is Element of the carrier of L
{S,FS} is non empty Element of bool the carrier of L
bool the carrier of L is non empty V271() set
S is Element of the carrier of L
FS is Element of the carrier of L
{S,FS} is non empty Element of bool the carrier of L
bool the carrier of L is non empty V271() set
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
A is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
the carrier of A is non empty set
D is Element of the carrier of A
FS is Element of the carrier of A
S is Element of the carrier of A
S "/\" FS is Element of the carrier of A
D "\/" (S "/\" FS) is Element of the carrier of A
D "\/" S is Element of the carrier of A
(D "\/" S) "/\" FS is Element of the carrier of A
the carrier of L is non empty set
[: the carrier of L, the carrier of A:] is non empty set
bool [: the carrier of L, the carrier of A:] is non empty V271() set
FS is Relation-like the carrier of L -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier of L, the carrier of A:]
FS " is Relation-like Function-like set
(FS ") . FS is set
(FS ") . D is set
(FS ") . S is set
rng FS is Element of bool the carrier of A
bool the carrier of A is non empty V271() set
FS . ((FS ") . S) is set
dom FS is Element of bool the carrier of L
bool the carrier of L is non empty V271() set
FS . ((FS ") . D) is set
FS . ((FS ") . FS) is set
f is Element of the carrier of L
A9 is Element of the carrier of L
FD is Element of the carrier of L
FD "/\" A9 is Element of the carrier of L
f "\/" (FD "/\" A9) is Element of the carrier of L
f "\/" FD is Element of the carrier of L
(f "\/" FD) "/\" A9 is Element of the carrier of L
S "/\" FS is Element of the carrier of A
D "\/" (S "/\" FS) is Element of the carrier of A
FS . f is Element of the carrier of A
FS . (FD "/\" A9) is Element of the carrier of A
(FS . f) "\/" (FS . (FD "/\" A9)) is Element of the carrier of A
FS . ((f "\/" FD) "/\" A9) is Element of the carrier of A
FS . (f "\/" FD) is Element of the carrier of A
FS . A9 is Element of the carrier of A
(FS . (f "\/" FD)) "/\" (FS . A9) is Element of the carrier of A
D "\/" S is Element of the carrier of A
(D "\/" S) "/\" FS is Element of the carrier of A
L is non empty reflexive transitive antisymmetric lower-bounded RelStr
the carrier of L is non empty set
A is non empty reflexive transitive antisymmetric RelStr
the carrier of A is non empty set
[: the carrier of L, the carrier of A:] is non empty set
bool [: the carrier of L, the carrier of A:] is non empty V271() set
D is Relation-like the carrier of L -defined the carrier of A -valued Function-like quasi_total monotone Element of bool [: the carrier of L, the carrier of A:]
Image D is non empty strict reflexive transitive antisymmetric full SubRelStr of A
rng D is Element of bool the carrier of A
bool the carrier of A is non empty V271() set
subrelstr (rng D) is strict reflexive transitive antisymmetric full SubRelStr of A
S is Element of the carrier of L
dom D is Element of bool the carrier of L
bool the carrier of L is non empty V271() set
D . S is Element of the carrier of A
the carrier of (Image D) is non empty set
FS is Element of the carrier of (Image D)
FS is Element of the carrier of (Image D)
the carrier of (subrelstr (rng D)) is set
FD is set
D . FD is set
FS is Element of the carrier of L
f is Element of the carrier of A
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
the carrier of L is non empty set
A is Element of the carrier of L
D is Element of the carrier of L
S is non empty set
EqRelLATT S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V227() with_suprema with_infima V297() RelStr
the carrier of (EqRelLATT S) is non empty set
[: the carrier of L, the carrier of (EqRelLATT S):] is non empty set
bool [: the carrier of L, the carrier of (EqRelLATT S):] is non empty V271() set
FS is Relation-like the carrier of L -defined the carrier of (EqRelLATT S) -valued Function-like quasi_total monotone meet-preserving join-preserving Element of bool [: the carrier of L, the carrier of (EqRelLATT S):]
Image FS is non empty strict reflexive transitive antisymmetric full meet-inheriting join-inheriting with_suprema with_infima SubRelStr of EqRelLATT S
rng FS is Element of bool the carrier of (EqRelLATT S)
bool the carrier of (EqRelLATT S) is non empty V271() set
subrelstr (rng FS) is strict reflexive transitive antisymmetric full SubRelStr of EqRelLATT S
the carrier of (Image FS) is non empty set
corestr FS is Relation-like the carrier of L -defined the carrier of (Image FS) -valued Function-like quasi_total onto monotone Element of bool [: the carrier of L, the carrier of (Image FS):]
[: the carrier of L, the carrier of (Image FS):] is non empty set
bool [: the carrier of L, the carrier of (Image FS):] is non empty V271() set
(corestr FS) . A is Element of the carrier of (Image FS)
(corestr FS) . D is Element of the carrier of (Image FS)
FS is Element of the carrier of L
FD is Element of the carrier of L
FS "/\" FD is Element of the carrier of L
(corestr FS) . (FS "/\" FD) is Element of the carrier of (Image FS)
(corestr FS) . FS is Element of the carrier of (Image FS)
(corestr FS) . FD is Element of the carrier of (Image FS)
((corestr FS) . FS) "/\" ((corestr FS) . FD) is Element of the carrier of (Image FS)
FS . FS is Element of the carrier of (EqRelLATT S)
FS . FD is Element of the carrier of (EqRelLATT S)
(FS . FS) "/\" (FS . FD) is Element of the carrier of (EqRelLATT S)
((corestr FS) . D) "/\" ((corestr FS) . A) is Element of the carrier of (Image FS)
A "/\" D is Element of the carrier of L
(corestr FS) . (A "/\" D) is Element of the carrier of (Image FS)
L is non empty non trivial set
EqRelLATT L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V227() with_suprema with_infima V297() RelStr
[:L,L:] is non empty set
bool [:L,L:] is non empty V271() set
id L is Relation-like L -defined L -valued Function-like one-to-one non empty total V72() V74() V75() V79() Element of bool [:L,L:]
A is non empty reflexive transitive antisymmetric full meet-inheriting join-inheriting with_suprema with_infima () SubRelStr of EqRelLATT L
the carrier of A is non empty set
type_of A is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
D is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
S is Element of the carrier of A
FS is Element of the carrier of A
FS is Element of the carrier of A
FS "/\" FS is Element of the carrier of A
S "\/" (FS "/\" FS) is Element of the carrier of A
S "\/" FS is Element of the carrier of A
(S "\/" FS) "/\" FS is Element of the carrier of A
the carrier of (EqRelLATT L) is non empty set
FD is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
f is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
FS is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
A9 is Element of the carrier of (EqRelLATT L)
f is Element of the carrier of (EqRelLATT L)
A9 "\/" f is Element of the carrier of (EqRelLATT L)
FD is Element of the carrier of (EqRelLATT L)
(A9 "\/" f) "/\" FD is Element of the carrier of (EqRelLATT L)
(A9 "\/" f) /\ f is Relation-like L -defined L -valued Element of bool [:L,L:]
FS "\/" FD is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
(FS "\/" FD) /\ f is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
f "/\" FD is Element of the carrier of (EqRelLATT L)
A9 "\/" (f "/\" FD) is Element of the carrier of (EqRelLATT L)
FD /\ f is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
FS "\/" (FD /\ f) is Relation-like L -defined L -valued total V72() V74() V79() Element of bool [:L,L:]
d9 is non empty set
[:d9,d9:] is non empty set
bool [:d9,d9:] is non empty V271() set
field D is set
Aq9 is Element of L
dq9 is Element of L
[Aq9,dq9] is non empty V25() set
{Aq9,dq9} is non empty set
{Aq9} is non empty trivial V47(1) set
{{Aq9,dq9},{Aq9}} is non empty set
[Aq9,dq9] is non empty V25() Element of [:L,L:]
2 + 2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q is Relation-like NAT -defined L -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of L
len q is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() Element of NAT
q . 4 is set
Q is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
2 * Q is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() even Element of NAT
(2 * Q) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() non even Element of NAT
q . 3 is set
3 + 1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q . (3 + 1) is set
[(q . 3),(q . (3 + 1))] is non empty V25() set
{(q . 3),(q . (3 + 1))} is non empty set
{(q . 3)} is non empty trivial V47(1) set
{{(q . 3),(q . (3 + 1))},{(q . 3)}} is non empty set
u is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
2 * u is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() even Element of NAT
q . 2 is set
2 + 1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q . (2 + 1) is set
[(q . 2),(q . (2 + 1))] is non empty V25() set
{(q . 2),(q . (2 + 1))} is non empty set
{(q . 2)} is non empty trivial V47(1) set
{{(q . 2),(q . (2 + 1))},{(q . 2)}} is non empty set
q . 1 is set
e is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
2 * e is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() even Element of NAT
(2 * e) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() non even Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q . (1 + 1) is set
[(q . 1),(q . (1 + 1))] is non empty V25() set
{(q . 1),(q . (1 + 1))} is non empty set
{(q . 1)} is non empty trivial V47(1) set
{{(q . 1),(q . (1 + 1))},{(q . 1)}} is non empty set
v is Element of the carrier of (EqRelLATT L)
A9 "\/" v is Element of the carrier of (EqRelLATT L)
v "\/" A9 is Element of the carrier of (EqRelLATT L)
[dq9,Aq9] is non empty V25() Element of [:L,L:]
{dq9,Aq9} is non empty set
{dq9} is non empty trivial V47(1) set
{{dq9,Aq9},{dq9}} is non empty set
[(q . 3),Aq9] is non empty V25() set
{(q . 3),Aq9} is non empty set
{{(q . 3),Aq9},{(q . 3)}} is non empty set
[(q . 3),(q . 2)] is non empty V25() set
{(q . 3),(q . 2)} is non empty set
{{(q . 3),(q . 2)},{(q . 3)}} is non empty set
[(q . 2),(q . 3)] is non empty V25() set
{(q . 2),(q . 3)} is non empty set
{{(q . 2),(q . 3)},{(q . 2)}} is non empty set
[Aq9,(q . 3)] is non empty V25() set
{Aq9,(q . 3)} is non empty set
{{Aq9,(q . 3)},{Aq9}} is non empty set
1 + 2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q is Relation-like NAT -defined L -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of L
len q is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() Element of NAT
q . 2 is set
u is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
2 * a is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() even Element of NAT
(2 * a) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() non even Element of NAT
q . 1 is set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q . (1 + 1) is set
[(q . 1),(q . (1 + 1))] is non empty V25() set
{(q . 1),(q . (1 + 1))} is non empty set
{(q . 1)} is non empty trivial V47(1) set
{{(q . 1),(q . (1 + 1))},{(q . 1)}} is non empty set
2 * u is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() even Element of NAT
2 + 1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q . (2 + 1) is set
[(q . 2),(q . (2 + 1))] is non empty V25() set
{(q . 2),(q . (2 + 1))} is non empty set
{(q . 2)} is non empty trivial V47(1) set
{{(q . 2),(q . (2 + 1))},{(q . 2)}} is non empty set
v is Element of the carrier of (EqRelLATT L)
A9 "\/" v is Element of the carrier of (EqRelLATT L)
[(q . 2),Aq9] is non empty V25() set
{(q . 2),Aq9} is non empty set
{{(q . 2),Aq9},{(q . 2)}} is non empty set
[(q . 2),dq9] is non empty V25() set
{(q . 2),dq9} is non empty set
{{(q . 2),dq9},{(q . 2)}} is non empty set
v "\/" A9 is Element of the carrier of (EqRelLATT L)
q . 3 is set
0 + 2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q is Relation-like NAT -defined L -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of L
len q is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() Element of NAT
u is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
2 * u is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() even Element of NAT
(2 * u) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() non even Element of NAT
q . 1 is set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
q . (1 + 1) is set
[(q . 1),(q . (1 + 1))] is non empty V25() set
{(q . 1),(q . (1 + 1))} is non empty set
{(q . 1)} is non empty trivial V47(1) set
{{(q . 1),(q . (1 + 1))},{(q . 1)}} is non empty set
Q is Element of the carrier of (EqRelLATT L)
A9 "\/" Q is Element of the carrier of (EqRelLATT L)
q . 2 is set
S "\/" FS is Element of the carrier of A
(S "\/" FS) "/\" FS is Element of the carrier of A
FS "/\" FS is Element of the carrier of A
S "\/" (FS "/\" FS) is Element of the carrier of A
L is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
the carrier of L is non empty set
A is non empty non trivial set
EqRelLATT A is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V227() with_suprema with_infima V297() RelStr
the carrier of (EqRelLATT A) is non empty set
[: the carrier of L, the carrier of (EqRelLATT A):] is non empty set
bool [: the carrier of L, the carrier of (EqRelLATT A):] is non empty V271() set
D is Relation-like the carrier of L -defined the carrier of (EqRelLATT A) -valued Function-like quasi_total monotone meet-preserving join-preserving Element of bool [: the carrier of L, the carrier of (EqRelLATT A):]
Image D is non empty strict reflexive transitive antisymmetric full meet-inheriting join-inheriting with_suprema with_infima SubRelStr of EqRelLATT A
rng D is Element of bool the carrier of (EqRelLATT A)
bool the carrier of (EqRelLATT A) is non empty V271() set
subrelstr (rng D) is strict reflexive transitive antisymmetric full SubRelStr of EqRelLATT A
[:A,A:] is non empty set
bool [:A,A:] is non empty V271() set
the carrier of (Image D) is non empty set
id A is Relation-like A -defined A -valued Function-like one-to-one non empty total V72() V74() V75() V79() Element of bool [:A,A:]
type_of (Image D) is epsilon-transitive epsilon-connected ordinal natural V33() V34() ext-real V38() V40() V45() Element of NAT
corestr D is Relation-like the carrier of L -defined the carrier of (Image D) -valued Function-like quasi_total onto monotone Element of bool [: the carrier of L, the carrier of (Image D):]
[: the carrier of L, the carrier of (Image D):] is non empty set
bool [: the carrier of L, the carrier of (Image D):] is non empty V271() set
rng (corestr D) is Element of bool the carrier of (Image D)
bool the carrier of (Image D) is non empty V271() set
S is Element of the carrier of L
FS is Element of the carrier of L
(corestr D) . S is Element of the carrier of (Image D)
(corestr D) . FS is Element of the carrier of (Image D)
S is Element of the carrier of L
(corestr D) . S is Element of the carrier of (Image D)
FS is Element of the carrier of L
(corestr D) . FS is Element of the carrier of (Image D)
S is Relation-like A -defined A -valued total V72() V74() V79() Element of bool [:A,A:]
L is set
{L} is non empty trivial V47(1) set
{{L}} is non empty trivial V47(1) set
{{L},{{L}}} is non empty set
L \/ {{L},{{L}}} is non empty set
L is set
(L) is set
{L} is non empty trivial V47(1) set
{{L}} is non empty trivial V47(1) set
{{L},{{L}}} is non empty set
L \/ {{L},{{L}}} is non empty set
L is non empty set
[:L,L:] is non empty set
A is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
the carrier of A is non empty set
[:[:L,L:], the carrier of A:] is non empty set
bool [:[:L,L:], the carrier of A:] is non empty V271() set
[:L,L, the carrier of A, the carrier of A:] is non empty set
(L) is non empty set
{L} is non empty trivial V47(1) set
{{L}} is non empty trivial V47(1) set
{{L},{{L}}} is non empty set
L \/ {{L},{{L}}} is non empty set
[:(L),(L):] is non empty set
[:[:(L),(L):], the carrier of A:] is non empty set
bool [:[:(L),(L):], the carrier of A:] is non empty V271() set
D is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:L,L:], the carrier of A:]
Bottom A is Element of the carrier of A
"\/" ({},A) is Element of the carrier of A
S is Element of [:L,L, the carrier of A, the carrier of A:]
S `1_4 is Element of L
S `1 is set
(S `1) `1 is set
((S `1) `1) `1 is set
S `2_4 is Element of L
((S `1) `1) `2 is set
D . ((S `1_4),(S `2_4)) is Element of the carrier of A
[(S `1_4),(S `2_4)] is non empty V25() set
{(S `1_4),(S `2_4)} is non empty set
{(S `1_4)} is non empty trivial V47(1) set
{{(S `1_4),(S `2_4)},{(S `1_4)}} is non empty set
D . [(S `1_4),(S `2_4)] is set
S `3_4 is Element of the carrier of A
(S `1) `2 is set
(D . ((S `1_4),(S `2_4))) "\/" (S `3_4) is Element of the carrier of A
S `4_4 is Element of the carrier of A
((D . ((S `1_4),(S `2_4))) "\/" (S `3_4)) "/\" (S `4_4) is Element of the carrier of A
FS is Element of the carrier of A
(D . ((S `1_4),(S `2_4))) "\/" FS is Element of the carrier of A
FS is Element of the carrier of A
((D . ((S `1_4),(S `2_4))) "\/" FS) "/\" FS is Element of the carrier of A
FS is Element of (L)
f is Element of (L)
D . (FS,f) is set
[FS,f] is non empty V25() set
{FS,f} is non empty set
{FS} is non empty trivial V47(1) set
{{FS,f},{FS}} is non empty set
D . [FS,f] is set
FD is Element of L
A9 is Element of L
D . (FD,A9) is Element of the carrier of A
[FD,A9] is non empty V25() set
{FD,A9} is non empty set
{FD} is non empty trivial V47(1) set
{{FD,A9},{FD}} is non empty set
D . [FD,A9] is set
FD is Element of L
D . (FD,(S `1_4)) is Element of the carrier of A
[FD,(S `1_4)] is non empty V25() set
{FD,(S `1_4)} is non empty set
{FD} is non empty trivial V47(1) set
{{FD,(S `1_4)},{FD}} is non empty set
D . [FD,(S `1_4)] is set
(D . (FD,(S `1_4))) "\/" FS is Element of the carrier of A
FD is Element of L
D . (FD,(S `2_4)) is Element of the carrier of A
[FD,(S `2_4)] is non empty V25() set
{FD,(S `2_4)} is non empty set
{FD} is non empty trivial V47(1) set
{{FD,(S `2_4)},{FD}} is non empty set
D . [FD,(S `2_4)] is set
(D . (FD,(S `2_4))) "\/" FS is Element of the carrier of A
FD is Element of L
D . (FD,(S `1_4)) is Element of the carrier of A
[FD,(S `1_4)] is non empty V25() set
{FD,(S `1_4)} is non empty set
{FD} is non empty trivial V47(1) set
{{FD,(S `1_4)},{FD}} is non empty set
D . [FD,(S `1_4)] is set
(D . (FD,(S `1_4))) "\/" FS is Element of the carrier of A
FD is Element of L
D . (FD,(S `2_4)) is Element of the carrier of A
[FD,(S `2_4)] is non empty V25() set
{FD,(S `2_4)} is non empty set
{FD} is non empty trivial V47(1) set
{{FD,(S `2_4)},{FD}} is non empty set
D . [FD,(S `2_4)] is set
(D . (FD,(S `2_4))) "\/" FS is Element of the carrier of A
FS is Relation-like [:(L),(L):] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:(L),(L):], the carrier of A:]
f is Relation-like [:(L),(L):] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:(L),(L):], the carrier of A:]
FD is Element of L
f . ({L},FD) is set
[{L},FD] is non empty V25() set
{{L},FD} is non empty set
{{{L},FD},{{L}}} is non empty set
f . [{L},FD] is set
D . (FD,(S `1_4)) is Element of the carrier of A
[FD,(S `1_4)] is non empty V25() set
{FD,(S `1_4)} is non empty set
{FD} is non empty trivial V47(1) set
{{FD,(S `1_4)},{FD}} is non empty set
D . [FD,(S `1_4)] is set
(D . (FD,(S `1_4))) "\/" FS is Element of the carrier of A
f . ({{L}},FD) is set
[{{L}},FD] is non empty V25() set
{{{L}},FD} is non empty set
{{{L}}} is non empty trivial V47(1) set
{{{{L}},FD},{{{L}}}} is non empty set
f . [{{L}},FD] is set
D . (FD,(S `2_4)) is Element of the carrier of A
[FD,(S `2_4)] is non empty V25() set
{FD,(S `2_4)} is non empty set
{{FD,(S `2_4)},{FD}} is non empty set
D . [FD,(S `2_4)] is set
(D . (FD,(S `2_4))) "\/" FS is Element of the carrier of A
A9 is Element of (L)
f . ({L},A9) is set
[{L},A9] is non empty V25() set
{{L},A9} is non empty set
{{{L},A9},{{L}}} is non empty set
f . [{L},A9] is set
d9 is Element of L
D . (d9,(S `1_4)) is Element of the carrier of A
[d9,(S `1_4)] is non empty V25() set
{d9,(S `1_4)} is non empty set
{d9} is non empty trivial V47(1) set
{{d9,(S `1_4)},{d9}} is non empty set
D . [d9,(S `1_4)] is set
(D . (d9,(S `1_4))) "\/" FS is Element of the carrier of A
f . ({{L}},A9) is set
[{{L}},A9] is non empty V25() set
{{{L}},A9} is non empty set
{{{{L}},A9},{{{L}}}} is non empty set
f . [{{L}},A9] is set
d9 is Element of L
D . (d9,(S `2_4)) is Element of the carrier of A
[d9,(S `2_4)] is non empty V25() set
{d9,(S `2_4)} is non empty set
{d9} is non empty trivial V47(1) set
{{d9,(S `2_4)},{d9}} is non empty set
D . [d9,(S `2_4)] is set
(D . (d9,(S `2_4))) "\/" FS is Element of the carrier of A
f . ({L},{L}) is set
[{L},{L}] is non empty V25() set
{{L},{L}} is non empty set
{{{L},{L}},{{L}}} is non empty set
f . [{L},{L}] is set
f . ({{L}},{{L}}) is set
[{{L}},{{L}}] is non empty V25() set
{{{L}},{{L}}} is non empty set
{{{L}}} is non empty trivial V47(1) set
{{{{L}},{{L}}},{{{L}}}} is non empty set
f . [{{L}},{{L}}] is set
f . ({L},{{L}}) is set
[{L},{{L}}] is non empty V25() set
{{{L},{{L}}},{{L}}} is non empty set
f . [{L},{{L}}] is set
f . ({{L}},{L}) is set
[{{L}},{L}] is non empty V25() set
{{{L}},{L}} is non empty set
{{{{L}},{L}},{{{L}}}} is non empty set
f . [{{L}},{L}] is set
FD is Element of L
A9 is Element of L
f . (FD,A9) is set
[FD,A9] is non empty V25() set
{FD,A9} is non empty set
{FD} is non empty trivial V47(1) set
{{FD,A9},{FD}} is non empty set
f . [FD,A9] is set
D . (FD,A9) is Element of the carrier of A
D . [FD,A9] is set
d9 is Element of (L)
Aq9 is Element of (L)
f . (d9,Aq9) is Element of the carrier of A
[d9,Aq9] is non empty V25() set
{d9,Aq9} is non empty set
{d9} is non empty trivial V47(1) set
{{d9,Aq9},{d9}} is non empty set
f . [d9,Aq9] is set
FD is Element of L
f . (FD,{L}) is set
[FD,{L}] is non empty V25() set
{FD,{L}} is non empty set
{FD} is non empty trivial V47(1) set
{{FD,{L}},{FD}} is non empty set
f . [FD,{L}] is set
D . (FD,(S `1_4)) is Element of the carrier of A
[FD,(S `1_4)] is non empty V25() set
{FD,(S `1_4)} is non empty set
{{FD,(S `1_4)},{FD}} is non empty set
D . [FD,(S `1_4)] is set
(D . (FD,(S `1_4))) "\/" FS is Element of the carrier of A
f . (FD,{{L}}) is set
[FD,{{L}}] is non empty V25() set
{FD,{{L}}} is non empty set
{{FD,{{L}}},{FD}} is non empty set
f . [FD,{{L}}] is set
D . (FD,(S `2_4)) is Element of the carrier of A
[FD,(S `2_4)] is non empty V25() set
{FD,(S `2_4)} is non empty set
{{FD,(S `2_4)},{FD}} is non empty set
D . [FD,(S `2_4)] is set
(D . (FD,(S `2_4))) "\/" FS is Element of the carrier of A
A9 is Element of (L)
f . (A9,{L}) is set
[A9,{L}] is non empty V25() set
{A9,{L}} is non empty set
{A9} is non empty trivial V47(1) set
{{A9,{L}},{A9}} is non empty set
f . [A9,{L}] is set
d9 is Element of L
D . (d9,(S `1_4)) is Element of the carrier of A
[d9,(S `1_4)] is non empty V25() set
{d9,(S `1_4)} is non empty set
{d9} is non empty trivial V47(1) set
{{d9,(S `1_4)},{d9}} is non empty set
D . [d9,(S `1_4)] is set
(D . (d9,(S `1_4))) "\/" FS is Element of the carrier of A
f . (A9,{{L}}) is set
[A9,{{L}}] is non empty V25() set
{A9,{{L}}} is non empty set
{{A9,{{L}}},{A9}} is non empty set
f . [A9,{{L}}] is set
d9 is Element of L
D . (d9,(S `2_4)) is Element of the carrier of A
[d9,(S `2_4)] is non empty V25() set
{d9,(S `2_4)} is non empty set
{d9} is non empty trivial V47(1) set
{{d9,(S `2_4)},{d9}} is non empty set
D . [d9,(S `2_4)] is set
(D . (d9,(S `2_4))) "\/" FS is Element of the carrier of A
FD is Element of L
A9 is Element of L
f . (FD,A9) is set
[FD,A9] is non empty V25() set
{FD,A9} is non empty set
{FD} is non empty trivial V47(1) set
{{FD,A9},{FD}} is non empty set
f . [FD,A9] is set
D . (FD,A9) is Element of the carrier of A
D . [FD,A9] is set
d9 is Element of L
f . (d9,{L}) is set
[d9,{L}] is non empty V25() set
{d9,{L}} is non empty set
{d9} is non empty trivial V47(1) set
{{d9,{L}},{d9}} is non empty set
f . [d9,{L}] is set
D . (d9,(S `1_4)) is Element of the carrier of A
[d9,(S `1_4)] is non empty V25() set
{d9,(S `1_4)} is non empty set
{{d9,(S `1_4)},{d9}} is non empty set
D . [d9,(S `1_4)] is set
(D . (d9,(S `1_4))) "\/" (S `3_4) is Element of the carrier of A
Aq9 is Element of L
f . ({L},Aq9) is set
[{L},Aq9] is non empty V25() set
{{L},Aq9} is non empty set
{{{L},Aq9},{{L}}} is non empty set
f . [{L},Aq9] is set
D . (Aq9,(S `1_4)) is Element of the carrier of A
[Aq9,(S `1_4)] is non empty V25() set
{Aq9,(S `1_4)} is non empty set
{Aq9} is non empty trivial V47(1) set
{{Aq9,(S `1_4)},{Aq9}} is non empty set
D . [Aq9,(S `1_4)] is set
(D . (Aq9,(S `1_4))) "\/" (S `3_4) is Element of the carrier of A
dq9 is Element of L
f . (dq9,{{L}}) is set
[dq9,{{L}}] is non empty V25() set
{dq9,{{L}}} is non empty set
{dq9} is non empty trivial V47(1) set
{{dq9,{{L}}},{dq9}} is non empty set
f . [dq9,{{L}}] is set
D . (dq9,(S `2_4)) is Element of the carrier of A
[dq9,(S `2_4)] is non empty V25() set
{dq9,(S `2_4)} is non empty set
{{dq9,(S `2_4)},{dq9}} is non empty set
D . [dq9,(S `2_4)] is set
(D . (dq9,(S `2_4))) "\/" (S `3_4) is Element of the carrier of A
q is Element of L
f . ({{L}},q) is set
[{{L}},q] is non empty V25() set
{{{L}},q} is non empty set
{{{{L}},q},{{{L}}}} is non empty set
f . [{{L}},q] is set
D . (q,(S `2_4)) is Element of the carrier of A
[q,(S `2_4)] is non empty V25() set
{q,(S `2_4)} is non empty set
{q} is non empty trivial V47(1) set
{{q,(S `2_4)},{q}} is non empty set
D . [q,(S `2_4)] is set
(D . (q,(S `2_4))) "\/" (S `3_4) is Element of the carrier of A
f is Relation-like [:(L),(L):] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:(L),(L):], the carrier of A:]
f . ({L},{L}) is set
[{L},{L}] is non empty V25() set
{{L},{L}} is non empty set
{{{L},{L}},{{L}}} is non empty set
f . [{L},{L}] is set
f . ({{L}},{{L}}) is set
[{{L}},{{L}}] is non empty V25() set
{{{L}},{{L}}} is non empty set
{{{L}}} is non empty trivial V47(1) set
{{{{L}},{{L}}},{{{L}}}} is non empty set
f . [{{L}},{{L}}] is set
f . ({L},{{L}}) is set
[{L},{{L}}] is non empty V25() set
{{{L},{{L}}},{{L}}} is non empty set
f . [{L},{{L}}] is set
f . ({{L}},{L}) is set
[{{L}},{L}] is non empty V25() set
{{{L}},{L}} is non empty set
{{{{L}},{L}},{{{L}}}} is non empty set
f . [{{L}},{L}] is set
FS is Relation-like [:(L),(L):] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:(L),(L):], the carrier of A:]
FS . ({L},{L}) is set
FS . [{L},{L}] is set
FS . ({{L}},{{L}}) is set
FS . [{{L}},{{L}}] is set
FS . ({L},{{L}}) is set
FS . [{L},{{L}}] is set
FS . ({{L}},{L}) is set
FS . [{{L}},{L}] is set
f is Element of (L)
FD is Element of (L)
f . (f,FD) is Element of the carrier of A
[f,FD] is non empty V25() set
{f,FD} is non empty set
{f} is non empty trivial V47(1) set
{{f,FD},{f}} is non empty set
f . [f,FD] is set
D . (f,FD) is set
D . [f,FD] is set
FS . (f,FD) is Element of the carrier of A
FS . [f,FD] is set
f . (f,FD) is Element of the carrier of A
[f,FD] is non empty V25() set
{f,FD} is non empty set
{f} is non empty trivial V47(1) set
{{f,FD},{f}} is non empty set
f . [f,FD] is set
A9 is Element of L
D . (A9,(S `1_4)) is Element of the carrier of A
[A9,(S `1_4)] is non empty V25() set
{A9,(S `1_4)} is non empty set
{A9} is non empty trivial V47(1) set
{{A9,(S `1_4)},{A9}} is non empty set
D . [A9,(S `1_4)] is set
(D . (A9,(S `1_4))) "\/" (S `3_4) is Element of the carrier of A
FS . (f,FD) is Element of the carrier of A
FS . [f,FD] is set
f . (f,FD) is Element of the carrier of A
[f,FD] is non empty V25() set
{f,FD} is non empty set
{f} is non empty trivial V47(1) set
{{f,FD},{f}} is non empty set
f . [f,FD] is set
A9 is Element of L
D . (A9,(S `2_4)) is Element of the carrier of A
[A9,(S `2_4)] is non empty V25() set
{A9,(S `2_4)} is non empty set
{A9} is non empty trivial V47(1) set
{{A9,(S `2_4)},{A9}} is non empty set
D . [A9,(S `2_4)] is set
(D . (A9,(S `2_4))) "\/" (S `3_4) is Element of the carrier of A
FS . (f,FD) is Element of the carrier of A
FS . [f,FD] is set
f . (f,FD) is Element of the carrier of A
[f,FD] is non empty V25() set
{f,FD} is non empty set
{f} is non empty trivial V47(1) set
{{f,FD},{f}} is non empty set
f . [f,FD] is set
A9 is Element of L
D . (A9,(S `1_4)) is Element of the carrier of A
[A9,(S `1_4)] is non empty V25() set
{A9,(S `1_4)} is non empty set
{A9} is non empty trivial V47(1) set
{{A9,(S `1_4)},{A9}} is non empty set
D . [A9,(S `1_4)] is set
(D . (A9,(S `1_4))) "\/" (S `3_4) is Element of the carrier of A
FS . (f,FD) is Element of the carrier of A
FS . [f,FD] is set
f . (f,FD) is Element of the carrier of A
[f,FD] is non empty V25() set
{f,FD} is non empty set
{f} is non empty trivial V47(1) set
{{f,FD},{f}} is non empty set
f . [f,FD] is set
FS . (f,FD) is Element of the carrier of A
FS . [f,FD] is set
f . (f,FD) is Element of the carrier of A
[f,FD] is non empty V25() set
{f,FD} is non empty set
{f} is non empty trivial V47(1) set
{{f,FD},{f}} is non empty set
f . [f,FD] is set
FS . (f,FD) is Element of the carrier of A
FS . [f,FD] is set
f . (f,FD) is Element of the carrier of A
[f,FD] is non empty V25() set
{f,FD} is non empty set
{f} is non empty trivial V47(1) set
{{f,FD},{f}} is non empty set
f . [f,FD] is set
A9 is Element of L
D . (A9,(S `2_4)) is Element of the carrier of A
[A9,(S `2_4)] is non empty V25() set
{A9,(S `2_4)} is non empty set
{A9} is non empty trivial V47(1) set
{{A9,(S `2_4)},{A9}} is non empty set
D . [A9,(S `2_4)] is set
(D . (A9,(S `2_4))) "\/" (S `3_4) is Element of the carrier of A
FS . (f,FD) is Element of the carrier of A
FS . [f,FD] is set
f . (f,FD) is Element of the carrier of A
[f,FD] is non empty V25() set
{f,FD} is non empty set
{f} is non empty trivial V47(1) set
{{f,FD},{f}} is non empty set
f . [f,FD] is set
FS . (f,FD) is Element of the carrier of A
FS . [f,FD] is set
f . (f,FD) is Element of the carrier of A
[f,FD] is non empty V25() set
{f,FD} is non empty set
{f} is non empty trivial V47(1) set
{{f,FD},{f}} is non empty set
f . [f,FD] is set
FS . (f,FD) is Element of the carrier of A
FS . [f,FD] is set
L is non empty set
[:L,L:] is non empty set
(L) is non empty set
{L} is non empty trivial V47(1) set
{{L}} is non empty trivial V47(1) set
{{L},{{L}}} is non empty set
L \/ {{L},{{L}}} is non empty set
A is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
the carrier of A is non empty set
[:[:L,L:], the carrier of A:] is non empty set
bool [:[:L,L:], the carrier of A:] is non empty V271() set
[:L,L, the carrier of A, the carrier of A:] is non empty set
D is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:L,L:], the carrier of A:]
S is Element of [:L,L, the carrier of A, the carrier of A:]
(L,A,D,S) is Relation-like [:(L),(L):] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:(L),(L):], the carrier of A:]
[:(L),(L):] is non empty set
[:[:(L),(L):], the carrier of A:] is non empty set
bool [:[:(L),(L):], the carrier of A:] is non empty V271() set
Bottom A is Element of the carrier of A
"\/" ({},A) is Element of the carrier of A
FS is Element of (L)
(L,A,D,S) . (FS,FS) is Element of the carrier of A
[FS,FS] is non empty V25() set
{FS,FS} is non empty set
{FS} is non empty trivial V47(1) set
{{FS,FS},{FS}} is non empty set
(L,A,D,S) . [FS,FS] is set
FD is Element of L
D . (FD,FD) is Element of the carrier of A
[FD,FD] is non empty V25() set
{FD,FD} is non empty set
{FD} is non empty trivial V47(1) set
{{FD,FD},{FD}} is non empty set
D . [FD,FD] is set
L is non empty set
[:L,L:] is non empty set
(L) is non empty set
{L} is non empty trivial V47(1) set
{{L}} is non empty trivial V47(1) set
{{L},{{L}}} is non empty set
L \/ {{L},{{L}}} is non empty set
A is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
the carrier of A is non empty set
[:[:L,L:], the carrier of A:] is non empty set
bool [:[:L,L:], the carrier of A:] is non empty V271() set
[:L,L, the carrier of A, the carrier of A:] is non empty set
D is Relation-like [:L,L:] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:L,L:], the carrier of A:]
S is Element of [:L,L, the carrier of A, the carrier of A:]
(L,A,D,S) is Relation-like [:(L),(L):] -defined the carrier of A -valued Function-like quasi_total Element of bool [:[:(L),(L):], the carrier of A:]
[:(L),(L):] is non empty set
[:[:(L),(L):], the carrier of A:] is non empty set
bool [:[:(L),(L):], the carrier of A:] is non empty V271() set
S `1_4 is Element of L
S `1 is set
(S `1) `1 is set
((S `1) `1) `1 is set
S `2_4 is Element of L
((S `1) `1) `2 is set
S `3_4 is Element of the carrier of A
(S `1) `2 is set
S `4_4 is Element of the carrier of A
f is Element of (L)
FD is Element of (L)
(L,A,D,S) . (f,FD) is Element of the carrier of A
[f,FD] is non empty V25() set
{f,FD} is non empty set
{f} is non empty trivial V47(1) set
{{f,FD},{f}} is non empty set
(L,A,D,S) . [f,FD] is set
(L,A,D,S) . (FD,f) is Element of the carrier of A
[FD,f] is non empty V25() set
{FD,f} is non empty set
{FD} is non empty trivial V47(1) set
{{FD,f},{FD}} is non empty set
(L,A,D,S) . [FD,f] is set
A9 is Element of L
d9 is Element of L
D . (A9,d9) is Element of the carrier of A
[A9,d9] is non empty V25() set
{A9,d9} is non empty set
{A9} is non empty trivial V47(1) set
{{A9,d9},{A9}} is non empty set
D . [A9,d9] is set
D . (d9,A9) is Element of the carrier of A
[d9,A9] is non empty V25() set
{d9,A9} is non empty set
{d9} is non empty trivial V47(1) set
{{d9,A9},{d9}} is non empty set
D . [d9,A9] is set
A9 is Element of L
D . (A9,(S `1_4)) is Element of the carrier of A
[A9,(S `1_4)] is non empty V25() set
{A9,(S `1_4)} is non empty set
{A9} is non empty trivial V47(1) set
{{A9,(S `1_4)},{A9}} is non empty set
D . [A9,(S `1_4)] is set
(D . (A9,(S `1_4))) "\/" (S `3_4) is Element of the carrier of A
A9 is Element of L
D . (A9,(S `2_4)) is Element of the carrier of A
[A9,(S `2_4)] is non empty V25() set
{A9,(S `2_4)} is non empty set
{A9} is non empty trivial V47(1) set
{{A9,(S `2_4)},{A9}} is non empty set
D . [A9,(S `2_4)] is set
(D . (A9,(S `2_4))) "\/" (S `3_4) is Element of the carrier of A
A9 is Element of L
D . (A9,(S `1_4)) is Element of the carrier of A
[A9,(S `1_4)] is non empty V25() set
{A9,(S `1_4)} is non empty set
{A9} is non empty trivial V47(1) set
{{A9,(S `1_4)},{A9}} is non empty set
D . [A9,(S `1_4)] is set
(D . (A9,(S `1_4))) "\/" (S `3_4) is Element of the carrier of A
D . ((S `1_4),(S `2_4)) is Element of the carrier of A
[(S `1_4),(S `2_4)] is non empty V25() set
{(S `1_4),(S `2_4)} is non empty set
{(S `1_4)} is non empty trivial V47(1) set
{{(S `1_4),(S `2_4)},{(S `1_4)}} is non empty set
D . [(S `1_4),(S `2_4)] is set
(D . ((S `1_4),(S `2_4))) "\/" (S `3_4) is Element of the carrier of A
((D . ((S `1_4),(S `2_4))) "\/" (S `3_4)) "/\" (S `4_4) is Element of the carrier of A
A9 is Element of L
D . (A9,(S `2_4)) is Element of the carrier of A
[A9,(S `2_4)] is non empty V25() set
{A9,(S `2_4)} is non empty set
{A9} is non empty trivial V47(1) set
{{A9,(S `2_4)},{A9}} is non empty set
D . [A9,(S `2_4)] is set
(D . (A9,(S `2_4))) "\/" (S `3_4) is Element of the carrier of A
D . ((S `1_4),(S `2_4)) is Element of the carrier of A
[(S `1_4),(S `2_4)] is non empty V25() set
{(S `1_4),(S `2_4)} is non empty set
{(S `1_4)} is non empty trivial V47(1) set
{{(S `1_4),(S `2_4)},{(S `1_4)}} is non empty set
D . [(S `1_4),(S `2_4)] is set
(D . ((S `1_4),(S `2_4))) "\/" (S `3_4) is Element of the carrier of A
((D . ((S `1_4),(S `2_4))) "\/" (S `3_4)) "/\" (S `4_4) is Element of the carrier of A
L is non empty set
[:L,L:] is non empty set
(L) is non empty set
{L} is non empty trivial V47(1) set
{{L}} is non empty trivial V47(1) set
{{L},{{L}}} is non empty set
L \/ {{L},{{L}}} is non empty set
A is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima RelStr
the carrier of A is non empty set
[:[:L,L:], the carrier of A:] is non empty set
bool [:[:L,L:], the carrier of A:] is non empty V271() set
[:L,L, the carrier of A, the carrier of A:] is non empty set
S is