:: 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
{ H₁(b₁,b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
{ H₁(b₁,b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u ) } 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
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,u,Z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u & b₂ in Z & b₁ tolerates b₂ ) } is set
{ H₁(b₁,b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : S₁[b₁,b₂] } is set
{ H₁(b₂,b₁) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : S₂[b₁,b₂] } is set
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₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u & b₂ in Z & b₁ tolerates b₂ ) } is set
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u & b₂ in {{}} & b₁ tolerates b₂ ) } 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)
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
Z is functional finite Element of (V,C)
(V,C,Z) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z \/ u or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z \/ u & b₂ c= b₁ ) ) ) ) ) } is set
(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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z) \/ u or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z) \/ u & b₂ c= b₁ ) ) ) ) ) } is set
Z \/ u is finite Element of Fin (PFuncs (V,C))
(V,C,(Z \/ u)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z \/ u or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z \/ u & b₂ c= b₁ ) ) ) ) ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in z & b₁ tolerates b₂ ) } is set
(V,C,u,z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u & b₂ in z & b₁ tolerates b₂ ) } is set
{ H₁(b₁,b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : S₁[b₁,b₂] } is set
{ H₁(b₁,b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : S₂[b₁,b₂] } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } 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)
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
u is finite Element of Fin (PFuncs (V,C))
(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z),u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in (V,C,Z) & b₂ in u & b₁ tolerates b₂ ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
u is finite Element of Fin (PFuncs (V,C))
(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,u)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,u) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,u) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,(V,C,Z),u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in (V,C,Z) & b₂ in u & b₁ tolerates b₂ ) } is 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))
z is finite Element of Fin (PFuncs (V,C))
(V,C,z,Z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in z & b₂ in Z & b₁ tolerates b₂ ) } is set
(V,C,z,u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in z & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,Z,z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in z & b₁ tolerates b₂ ) } is set
(V,C,u,z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u & b₂ in z & b₁ tolerates b₂ ) } 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
u is finite Element of Fin (PFuncs (V,C))
(V,C,(V,C,Z),u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in (V,C,Z) & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,(V,C,(V,C,Z),u)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,(V,C,Z),u) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,(V,C,Z),u) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,u)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,u) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,u) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in u or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,Z,(V,C,u)) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in (V,C,u) & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,(V,C,u))) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,(V,C,u)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,(V,C,u)) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,u)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,u) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,u) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,(V,C,u),Z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in (V,C,u) & b₂ in Z & b₁ tolerates b₂ ) } is set
(V,C,u,Z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u & b₂ in Z & b₁ tolerates b₂ ) } 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))
z is finite Element of Fin (PFuncs (V,C))
(V,C,u,z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u & b₂ in z & b₁ tolerates b₂ ) } is set
(V,C,Z,(V,C,u,z)) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in (V,C,u,z) & b₁ tolerates b₂ ) } is set
(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,u),z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in (V,C,Z,u) & b₂ in z & b₁ tolerates b₂ ) } is set
(V,C,z,u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in z & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,u,Z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u & b₂ in Z & b₁ tolerates b₂ ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in K & b₂ in M & b₁ tolerates b₂ ) } is set
(V,C,u9,(V,C,K,M)) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u9 & b₂ in (V,C,K,M) & b₁ tolerates b₂ ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u9 & b₂ in K & b₁ tolerates b₂ ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in (V,C,u9,K) & b₂ in M & b₁ tolerates b₂ ) } is set
(V,C,z,(V,C,Z,u)) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in z & b₂ in (V,C,Z,u) & b₁ tolerates b₂ ) } is set
(V,C,(V,C,u,z),Z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in (V,C,u,z) & b₂ in Z & b₁ tolerates b₂ ) } 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))
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u \/ z & b₁ tolerates b₂ ) } is set
(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,Z,z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in z & b₁ tolerates b₂ ) } is set
(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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
(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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,u) \/ u or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,u) \/ u & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,u) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in u or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u & b₂ c= b₁ ) ) ) ) ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in Z & b₁ tolerates b₂ ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in Z & b₁ tolerates b₂ ) } is set
(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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,Z) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,Z) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,Z) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
(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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,Z) \/ Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,Z) \/ Z & b₂ c= b₁ ) ) ) ) ) } 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
Z is functional finite Element of (V,C)
(V,C,Z,Z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in Z & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,Z)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,Z) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,Z) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,Z) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in Z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Z & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,z,u9) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,z,u9) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in K & b₂ in M & b₁ tolerates b₂ ) } is set
(V,C,(V,C,K,M)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,K,M) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,K,M) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,G,y) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,G,y) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in G & b₂ in y & b₁ tolerates b₂ ) } is set
(V,C,(V,C,G,y)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,G,y) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,G,y) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,K,u9) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,K,u9) & b₂ c= b₁ ) ) ) ) ) } 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 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,K,M) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,K,M) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,(V,C,(V,C,K,M)),u9) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,(V,C,(V,C,K,M)),u9) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in u9 \/ (V,C,K,M) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u9 \/ (V,C,K,M) & b₂ c= b₁ ) ) ) ) ) } is set
(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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,u9,K) \/ M or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,u9,K) \/ M & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,(V,C,u9,K)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,u9,K) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,u9,K) & b₂ c= b₁ ) ) ) ) ) } is set
(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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,(V,C,(V,C,u9,K)),M) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,(V,C,(V,C,u9,K)),M) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
(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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,u)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,u) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,u) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,(V,C,(V,C,Z,u)),u) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,(V,C,(V,C,Z,u)),u) & b₂ c= b₁ ) ) ) ) ) } is set
(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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,u) \/ u or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,u) \/ u & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,u) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in u or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u & b₂ c= b₁ ) ) ) ) ) } 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)
(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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in z & b₂ in u9 & b₁ tolerates b₂ ) } is set
(V,C,(V,C,z,u9)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,z,u9) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,z,u9) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,u9,z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u9 & b₂ in z & b₁ tolerates b₂ ) } is set
(V,C,(V,C,u9,z)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,u9,z) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,u9,z) & b₂ c= b₁ ) ) ) ) ) } 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 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in K & b₂ in M & b₁ tolerates b₂ ) } is set
(V,C,(V,C,K,M)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,K,M) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,K,M) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u9 & b₂ in (V,C,(V,C,K,M)) & b₁ tolerates b₂ ) } is set
(V,C,(V,C,u9,(V,C,(V,C,K,M)))) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,u9,(V,C,(V,C,K,M))) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,u9,(V,C,(V,C,K,M))) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,u9,(V,C,K,M)) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u9 & b₂ in (V,C,K,M) & b₁ tolerates b₂ ) } is set
(V,C,(V,C,u9,(V,C,K,M))) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,u9,(V,C,K,M)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,u9,(V,C,K,M)) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,u9,K) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u9 & b₂ in K & b₁ tolerates b₂ ) } is set
(V,C,(V,C,u9,K),M) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in (V,C,u9,K) & b₂ in M & b₁ tolerates b₂ ) } is set
(V,C,(V,C,(V,C,u9,K),M)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,(V,C,u9,K),M) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,(V,C,u9,K),M) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,(V,C,u9,K)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,u9,K) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,u9,K) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,(V,C,(V,C,u9,K)),M) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in (V,C,(V,C,u9,K)) & b₂ in M & b₁ tolerates b₂ ) } is set
(V,C,(V,C,(V,C,(V,C,u9,K)),M)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,(V,C,(V,C,u9,K)),M) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,(V,C,(V,C,u9,K)),M) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
(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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in z & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,z)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,z) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,z) & b₂ c= b₁ ) ) ) ) ) } is set
(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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,u,z) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,u,z) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,u)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,u) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,u) & b₂ c= b₁ ) ) ) ) ) } is set
u9 is functional finite Element of (V,C)
(V,C,Z,u9) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in u9 & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,u9)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,u9) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,u9) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,Z,(V,C,(V,C,u,z))) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in (V,C,(V,C,u,z)) & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,(V,C,(V,C,u,z)))) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,(V,C,(V,C,u,z))) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,(V,C,(V,C,u,z))) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,Z,(V,C,u,z)) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in (V,C,u,z) & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,(V,C,u,z))) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,(V,C,u,z)) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,(V,C,u,z)) & b₂ c= b₁ ) ) ) ) ) } is set
(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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,u) \/ (V,C,Z,z) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,u) \/ (V,C,Z,z) & b₂ c= b₁ ) ) ) ) ) } is set
(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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,(V,C,Z,u)) \/ (V,C,Z,z) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,(V,C,Z,u)) \/ (V,C,Z,z) & b₂ c= b₁ ) ) ) ) ) } is set
(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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,(V,C,(V,C,Z,u)),(V,C,(V,C,Z,z))) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,(V,C,(V,C,Z,u)),(V,C,(V,C,Z,z))) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,K,(V,C,(V,C,Z,z))) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,K,(V,C,(V,C,Z,z))) & b₂ c= b₁ ) ) ) ) ) } is set
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₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,K,M) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,K,M) & b₂ c= b₁ ) ) ) ) ) } 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_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 "\/" 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)))
the L_meet of (V,C) . (Z,(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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
z is functional finite Element of (V,C)
the L_meet of (V,C) . (z,z) is set
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,z)),( the L_meet of (V,C) . (z,u9))) is set
(V,C,z,z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in z & b₂ in z & b₁ tolerates b₂ ) } is set
(V,C,(V,C,z,z)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,z,z) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,z,z) & b₂ c= b₁ ) ) ) ) ) } is set
the L_join of (V,C) . ((V,C,(V,C,z,z)),( the L_meet of (V,C) . (z,u9))) is set
(V,C,z) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in z or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in z & b₂ c= b₁ ) ) ) ) ) } is set
the L_join of (V,C) . ((V,C,z),( the L_meet of (V,C) . (z,u9))) is set
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 "\/" (Z "/\" u) is Element of the carrier of (V,C)
the L_join of (V,C) . (Z,(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)
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)
(u "/\" Z) "\/" Z is Element of the carrier of (V,C)
the L_join of (V,C) . ((u "/\" Z),Z) is Element of the carrier of (V,C)
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)
u is Element of the carrier of (V,C)
z is Element of the carrier of (V,C)
u9 is Element of the carrier of (V,C)
z "\/" u9 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,u9) is Element of the carrier of (V,C)
u "\/" (z "\/" u9) is Element of the carrier of (V,C)
the L_join of (V,C) . (u,(z "\/" u9)) is Element of the carrier of (V,C)
u "\/" z is Element of the carrier of (V,C)
the L_join of (V,C) . (u,z) is Element of the carrier of (V,C)
(u "\/" z) "\/" u9 is Element of the carrier of (V,C)
the L_join of (V,C) . ((u "\/" z),u9) 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)
(u "/\" z) "\/" 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)))
the L_join of (V,C) . ((u "/\" z),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 is Element of the carrier of (V,C)
the L_meet of (V,C) . (z,u) 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)
u9 is Element of the carrier of (V,C)
z "/\" u9 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,u9) is Element of the carrier of (V,C)
u "/\" (z "/\" u9) is Element of the carrier of (V,C)
the L_meet of (V,C) . (u,(z "/\" u9)) 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)
(u "/\" z) "/\" u9 is Element of the carrier of (V,C)
the L_meet of (V,C) . ((u "/\" z),u9) 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)
u "/\" (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)))
the L_meet of (V,C) . (u,(u "\/" z)) is Element of the carrier of (V,C)
V is set
C is set
(V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like 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_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 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 "/\" z is Element of the carrier of (V,C)
the L_meet of (V,C) . (Z,z) is Element of the carrier of (V,C)
(Z "/\" u) "\/" (Z "/\" z) is Element of the carrier of (V,C)
the L_join of (V,C) . ((Z "/\" u),(Z "/\" 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
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)
u9 is functional finite Element of (V,C)
K is functional finite Element of (V,C)
M is functional finite Element of (V,C)
the L_join of (V,C) . (K,M) is set
the L_meet of (V,C) . (u9,( the L_join of (V,C) . (K,M))) is set
Z "/\" u is Element of the carrier of (V,C)
Z "/\" z is Element of the carrier of (V,C)
(Z "/\" u) "\/" (Z "/\" z) is Element of the carrier of (V,C)
the L_join of (V,C) . ((Z "/\" u),(Z "/\" 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
the carrier of (V,C) is set
Z is functional finite Element of (V,C)
z is Element of the carrier of (V,C)
u9 is Element of the carrier of (V,C)
z "/\" u9 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,u9) is Element of the carrier of (V,C)
u9 "/\" z is Element of the carrier of (V,C)
the L_meet of (V,C) . (u9,z) is Element of the carrier of (V,C)
z "\/" u9 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,u9) is Element of the carrier of (V,C)
K is functional finite Element of (V,C)
(V,C,Z,K) is finite Element of Fin (PFuncs (V,C))
(V,C,(V,C,Z,K)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,K) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,K) & b₂ c= b₁ ) ) ) ) ) } is set
u9 "/\" 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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
the carrier of (V,C) is set
Z is functional finite Element of (V,C)
z is Element of the carrier of (V,C)
u9 is Element of the carrier of (V,C)
z "\/" u9 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,u9) is Element of the carrier of (V,C)
u9 "\/" z is Element of the carrier of (V,C)
the L_join of (V,C) . (u9,z) is Element of the carrier of (V,C)
z "/\" u9 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)))
the L_meet of (V,C) . (z,u9) is Element of the carrier of (V,C)
K is functional finite Element of (V,C)
(V,C,Z,K) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in Z & b₂ in K & b₁ tolerates b₂ ) } is set
(V,C,(V,C,Z,K)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,Z,K) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,Z,K) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,K,Z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in K & b₂ in Z & b₁ tolerates b₂ ) } is set
(V,C,(V,C,K,Z)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,K,Z) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,K,Z) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,K) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in K or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in K & b₂ c= b₁ ) ) ) ) ) } is set
z "\/" u9 is Element of the carrier of (V,C)
V is set
C is set
(V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded LattStr
Bottom (V,C) is Element of the carrier of (V,C)
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } 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 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))
(V,C,(V,C,z,u9)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,z,u9) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,z,u9) & b₂ c= b₁ ) ) ) ) ) } is set
V is set
C is set
(V,C) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded LattStr
Top (V,C) is Element of the carrier of (V,C)
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₁ where b₁ is finite Element of Fin (PFuncs (V,C)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being V1() Function-like Element of PFuncs (V,C) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } 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 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₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in z & b₂ in u9 & b₁ tolerates b₂ ) } is set
(V,C,(V,C,z,u9)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,z,u9) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,z,u9) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,u9,z) is finite Element of Fin (PFuncs (V,C))
{ (b₁ \/ b₂) where b₁, b₂ is V1() Function-like Element of PFuncs (V,C) : ( b₁ in u9 & b₂ in z & b₁ tolerates b₂ ) } is set
(V,C,(V,C,u9,z)) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in (V,C,u9,z) or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in (V,C,u9,z) & b₂ c= b₁ ) ) ) ) ) } is set
(V,C,u9) is functional finite Element of (V,C)
{ b₁ where b₁ is V1() Function-like Element of PFuncs (V,C) : ( b₁ is finite & ( for b₂ being V1() Function-like Element of PFuncs (V,C) holds
( ( not b₂ in u9 or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in u9 & b₂ c= b₁ ) ) ) ) ) } is set