:: SUBSTLAT semantic presentation

K104() is set

1 is non empty 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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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))
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } is set
{ H1(b1,b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } is set
{ H1(b1,b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } is set
(V,C,u,Z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u & b2 in Z & b1 tolerates b2 ) } is set
{ H1(b1,b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : S1[b1,b2] } is set
{ H1(b2,b1) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : S2[b1,b2] } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u & b2 in Z & b1 tolerates b2 ) } is set
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u & b2 in & b1 tolerates b2 ) } 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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

Z is functional finite Element of (V,C)
(V,C,Z) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z \/ u or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z \/ u & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z) \/ u or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z) \/ u & b2 c= b1 ) ) ) ) )
}
is set

Z \/ u is finite Element of Fin (PFuncs (V,C))
(V,C,(Z \/ u)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z \/ u or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z \/ u & b2 c= b1 ) ) ) ) )
}
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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in z & b1 tolerates b2 ) } is set
(V,C,u,z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u & b2 in z & b1 tolerates b2 ) } is set
{ H1(b1,b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : S1[b1,b2] } is set
{ H1(b1,b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : S2[b1,b2] } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } 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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
is set

u is finite Element of Fin (PFuncs (V,C))
(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } is set
(V,C,(V,C,Z),u) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in (V,C,Z) & b2 in u & b1 tolerates b2 ) } 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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
is set

u is finite Element of Fin (PFuncs (V,C))
(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,u)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,u) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,u) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,(V,C,Z),u) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in (V,C,Z) & b2 in u & b1 tolerates b2 ) } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in z & b2 in Z & b1 tolerates b2 ) } is set
(V,C,z,u) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in z & b2 in u & b1 tolerates b2 ) } is set
(V,C,Z,z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in z & b1 tolerates b2 ) } is set
(V,C,u,z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u & b2 in z & b1 tolerates b2 ) } 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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in (V,C,Z) & b2 in u & b1 tolerates b2 ) } is set
(V,C,(V,C,(V,C,Z),u)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,(V,C,Z),u) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,(V,C,Z),u) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,u)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,u) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,u) & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in u or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in u & b2 c= b1 ) ) ) ) )
}
is set

(V,C,Z,(V,C,u)) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in (V,C,u) & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,(V,C,u))) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,(V,C,u)) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,(V,C,u)) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,u)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,u) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,u) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,(V,C,u),Z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in (V,C,u) & b2 in Z & b1 tolerates b2 ) } is set
(V,C,u,Z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u & b2 in Z & b1 tolerates b2 ) } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u & b2 in z & b1 tolerates b2 ) } is set
(V,C,Z,(V,C,u,z)) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in (V,C,u,z) & b1 tolerates b2 ) } is set
(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,u),z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in (V,C,Z,u) & b2 in z & b1 tolerates b2 ) } is set
(V,C,z,u) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in z & b2 in u & b1 tolerates b2 ) } is set
(V,C,u,Z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u & b2 in Z & b1 tolerates b2 ) } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in K & b2 in M & b1 tolerates b2 ) } is set
(V,C,u9,(V,C,K,M)) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u9 & b2 in (V,C,K,M) & b1 tolerates b2 ) } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u9 & b2 in K & b1 tolerates b2 ) } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in (V,C,u9,K) & b2 in M & b1 tolerates b2 ) } is set
(V,C,z,(V,C,Z,u)) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in z & b2 in (V,C,Z,u) & b1 tolerates b2 ) } is set
(V,C,(V,C,u,z),Z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in (V,C,u,z) & b2 in Z & b1 tolerates b2 ) } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u \/ z & b1 tolerates b2 ) } is set
(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } is set
(V,C,Z,z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in z & b1 tolerates b2 ) } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } 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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,u) \/ u or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,u) \/ u & b2 c= b1 ) ) ) ) )
}
is set

(V,C,u) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in u or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in u & b2 c= b1 ) ) ) ) )
}
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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in Z & b1 tolerates b2 ) } 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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in Z & b1 tolerates b2 ) } 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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,Z) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,Z) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,Z) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,Z) \/ Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,Z) \/ Z & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
is set

Z is functional finite Element of (V,C)
(V,C,Z,Z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in Z & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,Z)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,Z) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,Z) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,Z) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in Z or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in Z & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,z,u9) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,z,u9) & b2 c= b1 ) ) ) ) )
}
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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in K & b2 in M & b1 tolerates b2 ) } is set
(V,C,(V,C,K,M)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,K,M) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,K,M) & b2 c= b1 ) ) ) ) )
}
is set

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

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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,G,y) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,G,y) & b2 c= b1 ) ) ) ) )
}
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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in G & b2 in y & b1 tolerates b2 ) } is set
(V,C,(V,C,G,y)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,G,y) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,G,y) & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,K,u9) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,K,u9) & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,K,M) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,K,M) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,(V,C,(V,C,K,M)),u9) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,(V,C,(V,C,K,M)),u9) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in u9 \/ (V,C,K,M) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in u9 \/ (V,C,K,M) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,u9,K) \/ M or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,u9,K) \/ M & b2 c= b1 ) ) ) ) )
}
is set

(V,C,(V,C,u9,K)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,u9,K) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,u9,K) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,(V,C,(V,C,u9,K)),M) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,(V,C,(V,C,u9,K)),M) & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,u)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,u) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,u) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,(V,C,(V,C,Z,u)),u) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,(V,C,(V,C,Z,u)),u) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,u) \/ u or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,u) \/ u & b2 c= b1 ) ) ) ) )
}
is set

(V,C,u) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in u or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in u & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in z & b2 in u9 & b1 tolerates b2 ) } is set
(V,C,(V,C,z,u9)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,z,u9) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,z,u9) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,u9,z) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u9 & b2 in z & b1 tolerates b2 ) } is set
(V,C,(V,C,u9,z)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,u9,z) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,u9,z) & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in K & b2 in M & b1 tolerates b2 ) } is set
(V,C,(V,C,K,M)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,K,M) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,K,M) & b2 c= b1 ) ) ) ) )
}
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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u9 & b2 in (V,C,(V,C,K,M)) & b1 tolerates b2 ) } is set
(V,C,(V,C,u9,(V,C,(V,C,K,M)))) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,u9,(V,C,(V,C,K,M))) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,u9,(V,C,(V,C,K,M))) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,u9,(V,C,K,M)) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u9 & b2 in (V,C,K,M) & b1 tolerates b2 ) } is set
(V,C,(V,C,u9,(V,C,K,M))) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,u9,(V,C,K,M)) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,u9,(V,C,K,M)) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,u9,K) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in u9 & b2 in K & b1 tolerates b2 ) } is set
(V,C,(V,C,u9,K),M) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in (V,C,u9,K) & b2 in M & b1 tolerates b2 ) } is set
(V,C,(V,C,(V,C,u9,K),M)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,(V,C,u9,K),M) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,(V,C,u9,K),M) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,(V,C,u9,K)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,u9,K) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,u9,K) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,(V,C,(V,C,u9,K)),M) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in (V,C,(V,C,u9,K)) & b2 in M & b1 tolerates b2 ) } is set
(V,C,(V,C,(V,C,(V,C,u9,K)),M)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,(V,C,(V,C,u9,K)),M) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,(V,C,(V,C,u9,K)),M) & b2 c= b1 ) ) ) ) )
}
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
{ b1 where b1 is finite Element of Fin (PFuncs (V,C)) : ( ( for b2 being set holds
( not b2 in b1 or b2 is finite ) ) & ( for b2, b3 being V1() Function-like Element of PFuncs (V,C) holds
( not b2 in b1 or not b3 in b1 or not b2 c= b3 or b2 = b3 ) ) )
}
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))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in z & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,z)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,z) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,z) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,u,z) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,u,z) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,Z,u) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,u)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,u) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,u) & b2 c= b1 ) ) ) ) )
}
is set

u9 is functional finite Element of (V,C)
(V,C,Z,u9) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in u9 & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,u9)) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,u9) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,u9) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,Z,(V,C,(V,C,u,z))) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in (V,C,(V,C,u,z)) & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,(V,C,(V,C,u,z)))) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,(V,C,(V,C,u,z))) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,(V,C,(V,C,u,z))) & b2 c= b1 ) ) ) ) )
}
is set

(V,C,Z,(V,C,u,z)) is finite Element of Fin (PFuncs (V,C))
{ (b1 \/ b2) where b1, b2 is V1() Function-like Element of PFuncs (V,C) : ( b1 in Z & b2 in (V,C,u,z) & b1 tolerates b2 ) } is set
(V,C,(V,C,Z,(V,C,u,z))) is functional finite Element of (V,C)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,(V,C,u,z)) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,(V,C,u,z)) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,Z,u) \/ (V,C,Z,z) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,Z,u) \/ (V,C,Z,z) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,(V,C,Z,u)) \/ (V,C,Z,z) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,(V,C,Z,u)) \/ (V,C,Z,z) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,(V,C,(V,C,Z,u)),(V,C,(V,C,Z,z))) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,(V,C,(V,C,Z,u)),(V,C,(V,C,Z,z))) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,K,(V,C,(V,C,Z,z))) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,K,(V,C,(V,C,Z,z))) & b2 c= b1 ) ) ) ) )
}
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)
{ b1 where b1 is V1() Function-like Element of PFuncs (V,C) : ( b1 is finite & ( for b2 being V1() Function-like Element of PFuncs (V,C) holds
( ( not b2 in (V,C,K,M) or not b2 c= b1 or b2 = b1 ) & ( not b2 = b1 or ( b2 in (V,C,K,M) & b2 c= b1 ) ) ) ) )
}
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