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