:: LATTICE8 semantic presentation

REAL is set

bool REAL is non empty set

bool NAT is non empty V40() V271() set

RAT is set
INT is set
bool NAT is non empty V40() V271() set

{{},1} is non empty set

[:2,2:] is non empty set
[:[:2,2:],2:] is non empty set
bool [:[:2,2:],2:] is non empty V271() set

(2 * 0) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() non even Element of NAT

L is non empty non trivial set

the carrier of () 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

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 ()
D is Element of the carrier of ()
{A,D} is non empty Element of bool the carrier of ()
bool the carrier of () is non empty V271() set

the carrier of (subrelstr {A,D}) is non empty set
FD is Element of the carrier of ()
f is Element of the carrier of ()
{FD,f} is non empty Element of bool the carrier of ()
"/\" ({FD,f},()) is Element of the carrier of ()
A "/\" A is Element of the carrier of ()
A "/\" D is Element of the carrier of ()
D "/\" A is Element of the carrier of ()
D "/\" D is Element of the carrier of ()
FD is set

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

d9 . 2 is set
d9 . 1 is set

d9 . Aq9 is set

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

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 ()
d9 . 3 is set
d9 . 2 is set
d9 . 3 is set

d9 . Aq9 is set

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

A "\/" D is Element of the carrier of ()
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 ()
f is Element of the carrier of ()
{FD,f} is non empty Element of bool the carrier of ()
"\/" ({FD,f},()) is Element of the carrier of ()
A "\/" A is Element of the carrier of ()
A "\/" D is Element of the carrier of ()
D "\/" A is Element of the carrier of ()
D "\/" D is Element of the carrier of ()
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

L is non empty set
[:L,L:] is non empty set

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

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

[:L,L:] is non empty set
bool [:L,L:] is non empty V271() set

the carrier of A is non empty set
D is set
the carrier of () 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:]

the carrier of L is non empty set

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

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

the carrier of L is non empty set

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

rng D is Element of bool the carrier of A
bool the carrier of A is non empty V271() set

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 () is non empty set
FS is Element of the carrier of ()
FS is Element of the carrier of ()
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

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

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 V271() set
FS is Relation-like the carrier of L -defined the carrier of () -valued Function-like quasi_total monotone meet-preserving join-preserving Element of bool [: the carrier of L, the carrier of ():]

rng FS is Element of bool the carrier of ()
bool the carrier of () is non empty V271() set

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 ()
FS . FD is Element of the carrier of ()
(FS . FS) "/\" (FS . FD) is Element of the carrier of ()
((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

[:L,L:] is non empty set
bool [:L,L:] is non empty V271() set

the carrier of A is non empty set

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 () 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 ()
f is Element of the carrier of ()
A9 "\/" f is Element of the carrier of ()
FD is Element of the carrier of ()
(A9 "\/" f) "/\" FD is Element of the carrier of ()
(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 ()
A9 "\/" (f "/\" FD) is Element of the carrier of ()
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:]

q . 4 is set

(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

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

q . 2 is set

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

(2 * e) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() ext-real V38() V40() V45() non even 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 ()
A9 "\/" v is Element of the carrier of ()
v "\/" A9 is Element of the carrier of ()
[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

q . 2 is set

(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

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 . (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 ()
A9 "\/" v is Element of the carrier of ()
[(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 ()
q . 3 is set

(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

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 ()
A9 "\/" Q is Element of the carrier of ()
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

the carrier of L is non empty set
A is non empty non trivial 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 V271() set
D is Relation-like the carrier of L -defined the carrier of () -valued Function-like quasi_total monotone meet-preserving join-preserving Element of bool [: the carrier of L, the carrier of ():]

rng D is Element of bool the carrier of ()
bool the carrier of () is non empty V271() set

[:A,A:] is non empty set
bool [:A,A:] is non empty V271() set
the carrier of () is non empty set

corestr D is Relation-like the carrier of L -defined the carrier of () -valued Function-like quasi_total onto monotone Element of bool [: the carrier of L, the carrier of ():]
[: the carrier of L, the carrier of ():] is non empty set
bool [: the carrier of L, the carrier of ():] is non empty V271() set
rng () is Element of bool the carrier of ()
bool the carrier of () is non empty V271() set
S is Element of the carrier of L
FS is Element of the carrier of L
() . S is Element of the carrier of ()
() . FS is Element of the carrier of ()
S is Element of the carrier of L
() . S is Element of the carrier of ()
FS is Element of the carrier of L
() . FS is Element of the carrier of ()
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

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
is non empty trivial V47(1) set
{{{{L}},FD},} 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},} 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
is non empty trivial V47(1) set
{{{{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}},} 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},} 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
is non empty trivial V47(1) set
{{{{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}},} 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

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

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

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