:: SUBSTLAT semantic presentation

K104() is set

K19(K104()) is cup-closed diff-closed preBoolean set

1 is non empty set

{} is Function-like functional empty finite V39() set

the Function-like functional empty finite V39() set is Function-like functional empty finite V39() set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

( not b

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

u is set

z is finite Element of Fin (PFuncs (V,C))

V is set

C is set

(V,C) is Element of K19((Fin (PFuncs (V,C))))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

u is set

Z is set

z is finite Element of Fin (PFuncs (V,C))

V is set

C is set

(V,C) is Element of K19((Fin (PFuncs (V,C))))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

Z is set

u is V1() Function-like Element of PFuncs (V,C)

z is V1() Function-like Element of PFuncs (V,C)

{{}} is non empty finite V39() set

V is set

C is set

(V,C) is Element of K19((Fin (PFuncs (V,C))))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

Z is V1() Function-like Element of PFuncs (V,C)

u is V1() Function-like Element of PFuncs (V,C)

K20(V,C) is set

K19(K20(V,C)) is cup-closed diff-closed preBoolean set

Z is set

V is set

C is set

(V,C) is Element of K19((Fin (PFuncs (V,C))))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

Z is Element of (V,C)

u is Element of (V,C)

Z \/ u is set

Z \/ u is finite Element of Fin (PFuncs (V,C))

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

Z is Element of (V,C)

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

{ b

( ( not b

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

z is set

u9 is V1() Function-like Element of PFuncs (V,C)

z is set

u9 is V1() Function-like Element of PFuncs (V,C)

z is set

u9 is finite Element of Fin (PFuncs (V,C))

K is set

M is V1() Function-like Element of PFuncs (V,C)

K is V1() Function-like Element of PFuncs (V,C)

M is V1() Function-like Element of PFuncs (V,C)

G is V1() Function-like Element of PFuncs (V,C)

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

Z is finite Element of (V,C)

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

{ (b

{ H

{ H

K is set

M is V1() Function-like Element of PFuncs (V,C)

G is V1() Function-like Element of PFuncs (V,C)

M \/ G is set

K is set

M is V1() Function-like Element of PFuncs (V,C)

G is V1() Function-like Element of PFuncs (V,C)

M \/ G is set

K20(V,C) is set

K19(K20(V,C)) is cup-closed diff-closed preBoolean set

b1 is V1() Function-like set

c1 is V1() Function-like set

b1 +* c1 is V1() Function-like set

y is V1() V4(V) V5(C) Function-like Element of K19(K20(V,C))

c9 is V1() V4(V) V5(C) Function-like Element of K19(K20(V,C))

y \/ c9 is V1() V4(V) V5(C) Element of K19(K20(V,C))

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,u,Z) is finite Element of Fin (PFuncs (V,C))

{ (b

{ H

{ H

K is set

G is V1() Function-like Element of PFuncs (V,C)

M is V1() Function-like Element of PFuncs (V,C)

G \/ M is set

M is V1() Function-like Element of PFuncs (V,C)

G is V1() Function-like Element of PFuncs (V,C)

M \/ G is set

c9 is V1() Function-like Element of PFuncs (V,C)

y is V1() Function-like Element of PFuncs (V,C)

c9 \/ y is set

M is V1() Function-like Element of PFuncs (V,C)

G is V1() Function-like Element of PFuncs (V,C)

M \/ G is set

K is V1() Function-like Element of PFuncs (V,C)

M is V1() Function-like Element of PFuncs (V,C)

K \/ M is set

M \/ K is set

K is V1() Function-like Element of PFuncs (V,C)

M is V1() Function-like Element of PFuncs (V,C)

y is V1() Function-like Element of PFuncs (V,C)

G is V1() Function-like Element of PFuncs (V,C)

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

(V,C,u,Z) is finite Element of Fin (PFuncs (V,C))

{ (b

{ (b

z is set

u9 is V1() Function-like Element of PFuncs (V,C)

K is V1() Function-like Element of PFuncs (V,C)

u9 \/ K is set

K20(V,C) is set

K19(K20(V,C)) is cup-closed diff-closed preBoolean set

u9 is set

z is V1() Function-like Element of PFuncs (V,C)

K is V1() Function-like Element of PFuncs (V,C)

K \/ z is set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

Z is finite Element of Fin (PFuncs (V,C))

u is set

z is set

u9 is V1() Function-like Element of PFuncs (V,C)

K is V1() Function-like Element of PFuncs (V,C)

M is finite Element of Fin (PFuncs (V,C))

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

u is set

z is V1() Function-like Element of PFuncs (V,C)

z is set

u9 is V1() Function-like Element of PFuncs (V,C)

K is V1() Function-like Element of PFuncs (V,C)

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

z is set

V is set

C is set

PFuncs (V,C) is functional non empty set

K20(V,C) is set

K19(K20(V,C)) is cup-closed diff-closed preBoolean set

Z is V1() Function-like Element of PFuncs (V,C)

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

u is finite set

u9 is V1() Function-like Element of PFuncs (V,C)

K is V1() Function-like Element of PFuncs (V,C)

z is V1() Function-like Element of PFuncs (V,C)

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

u is set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

u is finite set

u9 is V1() Function-like Element of PFuncs (V,C)

K is V1() Function-like Element of PFuncs (V,C)

M is V1() Function-like Element of PFuncs (V,C)

u9 is V1() Function-like Element of PFuncs (V,C)

z is V1() Function-like Element of PFuncs (V,C)

u9 is V1() Function-like Element of PFuncs (V,C)

K is finite set

M is V1() Function-like Element of PFuncs (V,C)

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

Z is functional finite Element of (V,C)

(V,C,Z) is functional finite Element of (V,C)

{ b

( ( not b

u is set

z is finite set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

u is finite Element of Fin (PFuncs (V,C))

Z \/ u is finite Element of Fin (PFuncs (V,C))

(V,C,(Z \/ u)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,Z) \/ u is finite Element of Fin (PFuncs (V,C))

z is set

K is finite set

u9 is finite set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

u is finite Element of Fin (PFuncs (V,C))

(V,C,Z) \/ u is finite Element of Fin (PFuncs (V,C))

(V,C,((V,C,Z) \/ u)) is functional finite Element of (V,C)

{ b

( ( not b

Z \/ u is finite Element of Fin (PFuncs (V,C))

(V,C,(Z \/ u)) is functional finite Element of (V,C)

{ b

( ( not b

z is set

K is finite set

M is set

u9 is finite set

z is set

K is finite set

u9 is finite set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

z is finite Element of Fin (PFuncs (V,C))

(V,C,Z,z) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,u,z) is finite Element of Fin (PFuncs (V,C))

{ (b

{ H

{ H

M is V1() Function-like Element of PFuncs (V,C)

G is V1() Function-like Element of PFuncs (V,C)

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

z is set

u9 is V1() Function-like Element of PFuncs (V,C)

K is V1() Function-like Element of PFuncs (V,C)

u9 \/ K is set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

z is V1() Function-like Element of PFuncs (V,C)

Z is finite Element of Fin (PFuncs (V,C))

u9 is V1() Function-like Element of PFuncs (V,C)

u is finite Element of Fin (PFuncs (V,C))

z \/ u9 is set

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

u is finite Element of Fin (PFuncs (V,C))

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z),u) is finite Element of Fin (PFuncs (V,C))

{ (b

z is finite set

u9 is V1() Function-like Element of PFuncs (V,C)

K is V1() Function-like Element of PFuncs (V,C)

u9 \/ K is set

M is set

K20(V,C) is set

K19(K20(V,C)) is cup-closed diff-closed preBoolean set

c9 is V1() V4(V) V5(C) Function-like Element of K19(K20(V,C))

b1 is V1() V4(V) V5(C) Function-like Element of K19(K20(V,C))

G is V1() Function-like Element of PFuncs (V,C)

y is V1() Function-like Element of PFuncs (V,C)

G \/ y is set

G +* y is V1() Function-like set

c1 is V1() V4(V) V5(C) Function-like Element of K19(K20(V,C))

c9 \/ c1 is V1() V4(V) V5(C) Element of K19(K20(V,C))

b2 is V1() Function-like Element of PFuncs (V,C)

b12 is finite set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

u is finite Element of Fin (PFuncs (V,C))

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,u)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,(V,C,Z),u) is finite Element of Fin (PFuncs (V,C))

{ (b

z is set

u9 is finite set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

z is finite Element of Fin (PFuncs (V,C))

(V,C,z,Z) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,Z,z) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,u,z) is finite Element of Fin (PFuncs (V,C))

{ (b

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

u is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,Z),u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,(V,C,Z),u)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,u)) is functional finite Element of (V,C)

{ b

( ( not b

z is set

u9 is finite set

K is finite set

z is set

u9 is finite set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

(V,C,u) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

(V,C,Z,(V,C,u)) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,(V,C,u))) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,u)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,(V,C,u),Z) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,u,Z) is finite Element of Fin (PFuncs (V,C))

{ (b

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

z is finite Element of Fin (PFuncs (V,C))

(V,C,u,z) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,Z,(V,C,u,z)) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,u),z) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,u,Z) is finite Element of Fin (PFuncs (V,C))

{ (b

u9 is finite Element of Fin (PFuncs (V,C))

K is finite Element of Fin (PFuncs (V,C))

M is finite Element of Fin (PFuncs (V,C))

(V,C,K,M) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,u9,(V,C,K,M)) is finite Element of Fin (PFuncs (V,C))

{ (b

G is set

y is set

c9 is set

y \/ c9 is set

b1 is set

c1 is set

b1 \/ c1 is set

K20(V,C) is set

K19(K20(V,C)) is cup-closed diff-closed preBoolean set

b9 is V1() Function-like Element of PFuncs (V,C)

b19 is V1() Function-like Element of PFuncs (V,C)

b9 \/ b19 is set

b9 +* b19 is V1() Function-like set

b2 is V1() V4(V) V5(C) Function-like Element of K19(K20(V,C))

b12 is V1() V4(V) V5(C) Function-like Element of K19(K20(V,C))

b2 \/ b12 is V1() V4(V) V5(C) Element of K19(K20(V,C))

y \/ (b1 \/ c1) is set

y \/ b1 is set

(y \/ b1) \/ c1 is set

c2 is V1() Function-like Element of PFuncs (V,C)

(V,C,u9,K) is finite Element of Fin (PFuncs (V,C))

{ (b

c19 is V1() Function-like Element of PFuncs (V,C)

(V,C,(V,C,u9,K),M) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,z,(V,C,Z,u)) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,u,z),Z) is finite Element of Fin (PFuncs (V,C))

{ (b

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

z is finite Element of Fin (PFuncs (V,C))

u \/ z is finite Element of Fin (PFuncs (V,C))

(V,C,Z,(u \/ z)) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,Z,z) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,Z,u) \/ (V,C,Z,z) is finite Element of Fin (PFuncs (V,C))

u9 is set

K is set

M is set

K \/ M is set

y is V1() Function-like Element of PFuncs (V,C)

G is V1() Function-like Element of PFuncs (V,C)

c9 is V1() Function-like Element of PFuncs (V,C)

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

z is set

u9 is set

K is set

u9 \/ K is set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

u is finite Element of Fin (PFuncs (V,C))

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,Z,u) \/ u is finite Element of Fin (PFuncs (V,C))

(V,C,((V,C,Z,u) \/ u)) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

(V,C,u) is functional finite Element of (V,C)

{ b

( ( not b

z is set

u9 is finite set

u9 is set

z is set

u9 is finite set

K is set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z,Z) is finite Element of Fin (PFuncs (V,C))

{ (b

u is set

u \/ u is set

z is V1() Function-like Element of PFuncs (V,C)

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

Z is finite Element of Fin (PFuncs (V,C))

(V,C,Z,Z) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,Z)) is functional finite Element of (V,C)

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

{ b

( ( not b

(V,C,Z) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,Z,Z) \/ Z is finite Element of Fin (PFuncs (V,C))

(V,C,((V,C,Z,Z) \/ Z)) is functional finite Element of (V,C)

{ b

( ( not b

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

Z is functional finite Element of (V,C)

(V,C,Z,Z) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,Z)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,Z) is functional finite Element of (V,C)

{ b

( ( not b

V is set

C is set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

K20((V,C),(V,C)) is set

K20(K20((V,C),(V,C)),(V,C)) is set

K19(K20(K20((V,C),(V,C)),(V,C))) is cup-closed diff-closed preBoolean set

Z is V1() V4(K20((V,C),(V,C))) V5((V,C)) Function-like V18(K20((V,C),(V,C)),(V,C)) Element of K19(K20(K20((V,C),(V,C)),(V,C)))

u is V1() V4(K20((V,C),(V,C))) V5((V,C)) Function-like V18(K20((V,C),(V,C)),(V,C)) Element of K19(K20(K20((V,C),(V,C)),(V,C)))

LattStr(# (V,C),Z,u #) is non empty strict LattStr

the carrier of LattStr(# (V,C),Z,u #) is set

the L_join of LattStr(# (V,C),Z,u #) is V1() V4(K20( the carrier of LattStr(# (V,C),Z,u #), the carrier of LattStr(# (V,C),Z,u #))) V5( the carrier of LattStr(# (V,C),Z,u #)) Function-like V18(K20( the carrier of LattStr(# (V,C),Z,u #), the carrier of LattStr(# (V,C),Z,u #)), the carrier of LattStr(# (V,C),Z,u #)) Element of K19(K20(K20( the carrier of LattStr(# (V,C),Z,u #), the carrier of LattStr(# (V,C),Z,u #)), the carrier of LattStr(# (V,C),Z,u #)))

K20( the carrier of LattStr(# (V,C),Z,u #), the carrier of LattStr(# (V,C),Z,u #)) is set

K20(K20( the carrier of LattStr(# (V,C),Z,u #), the carrier of LattStr(# (V,C),Z,u #)), the carrier of LattStr(# (V,C),Z,u #)) is set

K19(K20(K20( the carrier of LattStr(# (V,C),Z,u #), the carrier of LattStr(# (V,C),Z,u #)), the carrier of LattStr(# (V,C),Z,u #))) is cup-closed diff-closed preBoolean set

the L_meet of LattStr(# (V,C),Z,u #) is V1() V4(K20( the carrier of LattStr(# (V,C),Z,u #), the carrier of LattStr(# (V,C),Z,u #))) V5( the carrier of LattStr(# (V,C),Z,u #)) Function-like V18(K20( the carrier of LattStr(# (V,C),Z,u #), the carrier of LattStr(# (V,C),Z,u #)), the carrier of LattStr(# (V,C),Z,u #)) Element of K19(K20(K20( the carrier of LattStr(# (V,C),Z,u #), the carrier of LattStr(# (V,C),Z,u #)), the carrier of LattStr(# (V,C),Z,u #)))

z is functional finite Element of (V,C)

u9 is functional finite Element of (V,C)

the L_join of LattStr(# (V,C),Z,u #) . (z,u9) is set

(V,C,z,u9) is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,z,u9)) is functional finite Element of (V,C)

{ b

( ( not b

K is functional finite Element of (V,C)

M is functional finite Element of (V,C)

the L_meet of LattStr(# (V,C),Z,u #) . (K,M) is set

(V,C,K,M) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,K,M)) is functional finite Element of (V,C)

{ b

( ( not b

Z is strict LattStr

the carrier of Z is set

the L_join of Z is V1() V4(K20( the carrier of Z, the carrier of Z)) V5( the carrier of Z) Function-like V18(K20( the carrier of Z, the carrier of Z), the carrier of Z) Element of K19(K20(K20( the carrier of Z, the carrier of Z), the carrier of Z))

K20( the carrier of Z, the carrier of Z) is set

K20(K20( the carrier of Z, the carrier of Z), the carrier of Z) is set

K19(K20(K20( the carrier of Z, the carrier of Z), the carrier of Z)) is cup-closed diff-closed preBoolean set

the L_meet of Z is V1() V4(K20( the carrier of Z, the carrier of Z)) V5( the carrier of Z) Function-like V18(K20( the carrier of Z, the carrier of Z), the carrier of Z) Element of K19(K20(K20( the carrier of Z, the carrier of Z), the carrier of Z))

u is strict LattStr

the carrier of u is set

the L_join of u is V1() V4(K20( the carrier of u, the carrier of u)) V5( the carrier of u) Function-like V18(K20( the carrier of u, the carrier of u), the carrier of u) Element of K19(K20(K20( the carrier of u, the carrier of u), the carrier of u))

K20( the carrier of u, the carrier of u) is set

K20(K20( the carrier of u, the carrier of u), the carrier of u) is set

K19(K20(K20( the carrier of u, the carrier of u), the carrier of u)) is cup-closed diff-closed preBoolean set

the L_meet of u is V1() V4(K20( the carrier of u, the carrier of u)) V5( the carrier of u) Function-like V18(K20( the carrier of u, the carrier of u), the carrier of u) Element of K19(K20(K20( the carrier of u, the carrier of u), the carrier of u))

K20((V,C),(V,C)) is set

K20(K20((V,C),(V,C)),(V,C)) is set

K19(K20(K20((V,C),(V,C)),(V,C))) is cup-closed diff-closed preBoolean set

K is V1() V4(K20((V,C),(V,C))) V5((V,C)) Function-like V18(K20((V,C),(V,C)),(V,C)) Element of K19(K20(K20((V,C),(V,C)),(V,C)))

G is functional finite Element of (V,C)

y is functional finite Element of (V,C)

K . (G,y) is functional finite Element of (V,C)

(V,C,G,y) is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,G,y)) is functional finite Element of (V,C)

{ b

( ( not b

M is V1() V4(K20((V,C),(V,C))) V5((V,C)) Function-like V18(K20((V,C),(V,C)),(V,C)) Element of K19(K20(K20((V,C),(V,C)),(V,C)))

M . (G,y) is functional finite Element of (V,C)

z is V1() V4(K20((V,C),(V,C))) V5((V,C)) Function-like V18(K20((V,C),(V,C)),(V,C)) Element of K19(K20(K20((V,C),(V,C)),(V,C)))

G is functional finite Element of (V,C)

y is functional finite Element of (V,C)

z . (G,y) is functional finite Element of (V,C)

(V,C,G,y) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,G,y)) is functional finite Element of (V,C)

{ b

( ( not b

u9 is V1() V4(K20((V,C),(V,C))) V5((V,C)) Function-like V18(K20((V,C),(V,C)),(V,C)) Element of K19(K20(K20((V,C),(V,C)),(V,C)))

u9 . (G,y) is functional finite Element of (V,C)

V is set

C is set

(V,C) is strict LattStr

the carrier of (V,C) is set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

V is set

C is set

(V,C) is non empty strict LattStr

the carrier of (V,C) is set

u is Element of the carrier of (V,C)

z is Element of the carrier of (V,C)

u "\/" z is Element of the carrier of (V,C)

the L_join of (V,C) is V1() V4(K20( the carrier of (V,C), the carrier of (V,C))) V5( the carrier of (V,C)) Function-like V18(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) Element of K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)))

K20( the carrier of (V,C), the carrier of (V,C)) is set

K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) is set

K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C))) is cup-closed diff-closed preBoolean set

the L_join of (V,C) . (u,z) is Element of the carrier of (V,C)

z "\/" u is Element of the carrier of (V,C)

the L_join of (V,C) . (z,u) is Element of the carrier of (V,C)

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

K is functional finite Element of (V,C)

u9 is functional finite Element of (V,C)

(V,C,K,u9) is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,K,u9)) is functional finite Element of (V,C)

{ b

( ( not b

V is set

C is set

(V,C) is non empty strict LattStr

the carrier of (V,C) is set

Z is Element of the carrier of (V,C)

u is Element of the carrier of (V,C)

z is Element of the carrier of (V,C)

u "\/" z is Element of the carrier of (V,C)

the L_join of (V,C) is V1() V4(K20( the carrier of (V,C), the carrier of (V,C))) V5( the carrier of (V,C)) Function-like V18(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) Element of K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)))

K20( the carrier of (V,C), the carrier of (V,C)) is set

K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) is set

K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C))) is cup-closed diff-closed preBoolean set

the L_join of (V,C) . (u,z) is Element of the carrier of (V,C)

Z "\/" (u "\/" z) is Element of the carrier of (V,C)

the L_join of (V,C) . (Z,(u "\/" z)) is Element of the carrier of (V,C)

Z "\/" u is Element of the carrier of (V,C)

the L_join of (V,C) . (Z,u) is Element of the carrier of (V,C)

(Z "\/" u) "\/" z is Element of the carrier of (V,C)

the L_join of (V,C) . ((Z "\/" u),z) is Element of the carrier of (V,C)

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

K is functional finite Element of (V,C)

M is functional finite Element of (V,C)

(V,C,K,M) is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,K,M)) is functional finite Element of (V,C)

{ b

( ( not b

the L_join of (V,C) . (Z,(V,C,(V,C,K,M))) is set

u9 is functional finite Element of (V,C)

(V,C,(V,C,(V,C,K,M)),u9) is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,(V,C,(V,C,K,M)),u9)) is functional finite Element of (V,C)

{ b

( ( not b

u9 \/ (V,C,K,M) is finite Element of Fin (PFuncs (V,C))

(V,C,(u9 \/ (V,C,K,M))) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,u9,K) is finite Element of Fin (PFuncs (V,C))

(V,C,u9,K) \/ M is finite Element of Fin (PFuncs (V,C))

(V,C,((V,C,u9,K) \/ M)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,(V,C,u9,K)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,(V,C,(V,C,u9,K)),M) is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,(V,C,(V,C,u9,K)),M)) is functional finite Element of (V,C)

{ b

( ( not b

the L_join of (V,C) . ((V,C,(V,C,u9,K)),M) is set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

(V,C) is non empty strict LattStr

the L_join of (V,C) is V1() V4(K20( the carrier of (V,C), the carrier of (V,C))) V5( the carrier of (V,C)) Function-like V18(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) Element of K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)))

the carrier of (V,C) is set

K20( the carrier of (V,C), the carrier of (V,C)) is set

K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) is set

K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C))) is cup-closed diff-closed preBoolean set

the L_meet of (V,C) is V1() V4(K20( the carrier of (V,C), the carrier of (V,C))) V5( the carrier of (V,C)) Function-like V18(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) Element of K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)))

Z is functional finite Element of (V,C)

u is functional finite Element of (V,C)

the L_meet of (V,C) . (Z,u) is set

the L_join of (V,C) . (( the L_meet of (V,C) . (Z,u)),u) is set

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,u)) is functional finite Element of (V,C)

{ b

( ( not b

the L_join of (V,C) . ((V,C,(V,C,Z,u)),u) is set

(V,C,(V,C,(V,C,Z,u)),u) is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,(V,C,(V,C,Z,u)),u)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,Z,u) \/ u is finite Element of Fin (PFuncs (V,C))

(V,C,((V,C,Z,u) \/ u)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,u) is functional finite Element of (V,C)

{ b

( ( not b

V is set

C is set

(V,C) is non empty strict LattStr

the carrier of (V,C) is set

Z is Element of the carrier of (V,C)

u is Element of the carrier of (V,C)

Z "/\" u is Element of the carrier of (V,C)

the L_meet of (V,C) is V1() V4(K20( the carrier of (V,C), the carrier of (V,C))) V5( the carrier of (V,C)) Function-like V18(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) Element of K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)))

K20( the carrier of (V,C), the carrier of (V,C)) is set

K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) is set

K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C))) is cup-closed diff-closed preBoolean set

the L_meet of (V,C) . (Z,u) is Element of the carrier of (V,C)

(Z "/\" u) "\/" u is Element of the carrier of (V,C)

the L_join of (V,C) is V1() V4(K20( the carrier of (V,C), the carrier of (V,C))) V5( the carrier of (V,C)) Function-like V18(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) Element of K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)))

the L_join of (V,C) . ((Z "/\" u),u) is Element of the carrier of (V,C)

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

z is functional finite Element of (V,C)

u9 is functional finite Element of (V,C)

the L_meet of (V,C) . (z,u9) is set

the L_join of (V,C) . (( the L_meet of (V,C) . (z,u9)),u9) is set

V is set

C is set

(V,C) is non empty strict LattStr

the carrier of (V,C) is set

Z is Element of the carrier of (V,C)

u is Element of the carrier of (V,C)

Z "/\" u is Element of the carrier of (V,C)

the L_meet of (V,C) is V1() V4(K20( the carrier of (V,C), the carrier of (V,C))) V5( the carrier of (V,C)) Function-like V18(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) Element of K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)))

K20( the carrier of (V,C), the carrier of (V,C)) is set

K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) is set

K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C))) is cup-closed diff-closed preBoolean set

the L_meet of (V,C) . (Z,u) is Element of the carrier of (V,C)

u "/\" Z is Element of the carrier of (V,C)

the L_meet of (V,C) . (u,Z) is Element of the carrier of (V,C)

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

z is functional finite Element of (V,C)

u9 is functional finite Element of (V,C)

(V,C,z,u9) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,z,u9)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,u9,z) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,u9,z)) is functional finite Element of (V,C)

{ b

( ( not b

V is set

C is set

(V,C) is non empty strict LattStr

the carrier of (V,C) is set

Z is Element of the carrier of (V,C)

u is Element of the carrier of (V,C)

z is Element of the carrier of (V,C)

u "/\" z is Element of the carrier of (V,C)

the L_meet of (V,C) is V1() V4(K20( the carrier of (V,C), the carrier of (V,C))) V5( the carrier of (V,C)) Function-like V18(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) Element of K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)))

K20( the carrier of (V,C), the carrier of (V,C)) is set

K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) is set

K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C))) is cup-closed diff-closed preBoolean set

the L_meet of (V,C) . (u,z) is Element of the carrier of (V,C)

Z "/\" (u "/\" z) is Element of the carrier of (V,C)

the L_meet of (V,C) . (Z,(u "/\" z)) is Element of the carrier of (V,C)

Z "/\" u is Element of the carrier of (V,C)

the L_meet of (V,C) . (Z,u) is Element of the carrier of (V,C)

(Z "/\" u) "/\" z is Element of the carrier of (V,C)

the L_meet of (V,C) . ((Z "/\" u),z) is Element of the carrier of (V,C)

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

K is functional finite Element of (V,C)

M is functional finite Element of (V,C)

(V,C,K,M) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,K,M)) is functional finite Element of (V,C)

{ b

( ( not b

the L_meet of (V,C) . (Z,(V,C,(V,C,K,M))) is set

u9 is functional finite Element of (V,C)

(V,C,u9,(V,C,(V,C,K,M))) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,u9,(V,C,(V,C,K,M)))) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,u9,(V,C,K,M)) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,u9,(V,C,K,M))) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,u9,K) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,u9,K),M) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,(V,C,u9,K),M)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,(V,C,u9,K)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,(V,C,(V,C,u9,K)),M) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,(V,C,(V,C,u9,K)),M)) is functional finite Element of (V,C)

{ b

( ( not b

the L_meet of (V,C) . ((V,C,(V,C,u9,K)),M) is set

V is set

C is set

PFuncs (V,C) is functional non empty set

Fin (PFuncs (V,C)) is non empty cup-closed diff-closed preBoolean set

(V,C) is non empty Element of K19((Fin (PFuncs (V,C))))

K19((Fin (PFuncs (V,C)))) is cup-closed diff-closed preBoolean set

{ b

( not b

( not b

(V,C) is non empty strict LattStr

the L_meet of (V,C) is V1() V4(K20( the carrier of (V,C), the carrier of (V,C))) V5( the carrier of (V,C)) Function-like V18(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) Element of K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)))

the carrier of (V,C) is set

K20( the carrier of (V,C), the carrier of (V,C)) is set

K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) is set

K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C))) is cup-closed diff-closed preBoolean set

the L_join of (V,C) is V1() V4(K20( the carrier of (V,C), the carrier of (V,C))) V5( the carrier of (V,C)) Function-like V18(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) Element of K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)))

Z is functional finite Element of (V,C)

u is functional finite Element of (V,C)

the L_meet of (V,C) . (Z,u) is set

z is functional finite Element of (V,C)

the L_join of (V,C) . (u,z) is set

the L_meet of (V,C) . (Z,( the L_join of (V,C) . (u,z))) is set

the L_meet of (V,C) . (Z,z) is set

the L_join of (V,C) . (( the L_meet of (V,C) . (Z,u)),( the L_meet of (V,C) . (Z,z))) is set

(V,C,Z,z) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,z)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,u,z) is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,u,z)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,u)) is functional finite Element of (V,C)

{ b

( ( not b

u9 is functional finite Element of (V,C)

(V,C,Z,u9) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,u9)) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,Z,(V,C,(V,C,u,z))) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,(V,C,(V,C,u,z)))) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,Z,(V,C,u,z)) is finite Element of Fin (PFuncs (V,C))

{ (b

(V,C,(V,C,Z,(V,C,u,z))) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,Z,u) \/ (V,C,Z,z) is finite Element of Fin (PFuncs (V,C))

(V,C,((V,C,Z,u) \/ (V,C,Z,z))) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,(V,C,Z,u)) \/ (V,C,Z,z) is finite Element of Fin (PFuncs (V,C))

(V,C,((V,C,(V,C,Z,u)) \/ (V,C,Z,z))) is functional finite Element of (V,C)

{ b

( ( not b

(V,C,(V,C,(V,C,Z,u)),(V,C,(V,C,Z,z))) is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,(V,C,(V,C,Z,u)),(V,C,(V,C,Z,z)))) is functional finite Element of (V,C)

{ b

( ( not b

K is functional finite Element of (V,C)

(V,C,K,(V,C,(V,C,Z,z))) is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,K,(V,C,(V,C,Z,z)))) is functional finite Element of (V,C)

{ b

( ( not b

M is functional finite Element of (V,C)

(V,C,K,M) is finite Element of Fin (PFuncs (V,C))

(V,C,(V,C,K,M)) is functional finite Element of (V,C)

{ b

( ( not b

V is set

C is set

(V,C) is non empty strict LattStr

the carrier of (V,C) is set

Z is Element of the carrier of (V,C)

u is Element of the carrier of (V,C)

Z "\/" u is Element of the carrier of (V,C)

the L_join of (V,C) is V1() V4(K20( the carrier of (V,C), the carrier of (V,C))) V5( the carrier of (V,C)) Function-like V18(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) Element of K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)))

K20( the carrier of (V,C), the carrier of (V,C)) is set

K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C)) is set

K19(K20(K20( the carrier of (V,C), the carrier of (V,C)), the carrier of (V,C))) is cup-closed diff-closed preBoolean set

the L_join of (V,C) . (Z,u) is Element of the carrier of (V,C)

Z "/\" (Z