:: WAYBEL18 semantic presentation

K108() is non finite countable denumerable Element of K19(K104())
K104() is set
K19(K104()) is non empty set
{} is Relation-like non-empty empty-yielding empty set
the Relation-like non-empty empty-yielding empty set is Relation-like non-empty empty-yielding empty set
1 is non empty set
{{},1} is non empty set
K103() is non finite countable denumerable set
K19(K103()) is non empty set
K19(K108()) is non empty set
I[01] is non empty strict TopSpace-like TopStruct
the carrier of I[01] is non empty set
K105() is set
K106() is set
K107() is set
K20(K104(),K104()) is Relation-like set
K19(K20(K104(),K104())) is non empty set
K472() is non empty V147() L13()
the carrier of K472() is non empty set
<REAL,+> is non empty V147() V169() V170() V171() V173() left-invertible right-invertible V225() left-cancelable right-cancelable V228() L13()
K478() is non empty V147() V171() V173() left-cancelable right-cancelable V228() SubStr of <REAL,+>
<NAT,+> is non empty V147() V169() V171() V173() left-cancelable right-cancelable V228() uniquely-decomposable SubStr of K478()
<REAL,*> is non empty V147() V169() V171() V173() L13()
<NAT,*> is non empty V147() V169() V171() V173() uniquely-decomposable SubStr of <REAL,*>
K523() is set
{{}} is non empty set
K443({{}}) is M23({{}})
K20(K443({{}}),{{}}) is Relation-like set
K19(K20(K443({{}}),{{}})) is non empty set
PFuncs (K443({{}}),{{}}) is set
K20(1,1) is Relation-like non empty set
K19(K20(1,1)) is non empty set
K20(K20(1,1),1) is Relation-like non empty set
K19(K20(K20(1,1),1)) is non empty set
union {} is set
T is set
K19(T) is non empty set
K19(K19(T)) is non empty set
J is Element of K19(K19(T))
M is Element of K19(K19(T))
M \ {{}} is Element of K19(K19(T))
J \/ {{}} is non empty set
UniCl M is Element of K19(K19(T))
UniCl J is Element of K19(K19(T))
PP is set
f is Element of K19(K19(T))
union f is Element of K19(T)
f \ {{}} is Element of K19(K19(T))
f is set
f is Element of K19(K19(T))
f \/ {{}} is non empty set
f \/ {{}} is non empty set
union (f \/ {{}}) is set
union {{}} is set
(union f) \/ (union {{}}) is set
(union f) \/ {} is set
union f is Element of K19(T)
(union f) \/ (union {{}}) is set
(union f) \/ {} is set
T is TopSpace-like TopStruct
the carrier of T is set
K19( the carrier of T) is non empty set
K19(K19( the carrier of T)) is non empty set
M is Element of K19(K19( the carrier of T))
M \ {{}} is Element of K19(K19( the carrier of T))
J is Element of K19(K19( the carrier of T))
UniCl J is Element of K19(K19( the carrier of T))
UniCl M is Element of K19(K19( the carrier of T))
the topology of T is non empty Element of K19(K19( the carrier of T))
PP is set
T is Relation-like Function-like set
M is set
dom T is set
T . M is set
rng T is set
T is set
the TopSpace-like TopStruct is TopSpace-like TopStruct
T --> the TopSpace-like TopStruct is Relation-like T -defined { the TopSpace-like TopStruct } -valued Function-like constant total quasi_total Element of K19(K20(T,{ the TopSpace-like TopStruct }))
{ the TopSpace-like TopStruct } is non empty set
K20(T,{ the TopSpace-like TopStruct }) is Relation-like set
K19(K20(T,{ the TopSpace-like TopStruct })) is non empty set
J is set
rng (T --> the TopSpace-like TopStruct ) is set
rng (T --> the TopSpace-like TopStruct ) is Element of K19({ the TopSpace-like TopStruct })
K19({ the TopSpace-like TopStruct }) is non empty set
T is set
the non empty TopSpace-like TopStruct is non empty TopSpace-like TopStruct
{ the non empty TopSpace-like TopStruct } is non empty set
K20(T,{ the non empty TopSpace-like TopStruct }) is Relation-like set
K19(K20(T,{ the non empty TopSpace-like TopStruct })) is non empty set
T --> the non empty TopSpace-like TopStruct is Relation-like T -defined { the non empty TopSpace-like TopStruct } -valued Function-like constant total quasi_total Element of K19(K20(T,{ the non empty TopSpace-like TopStruct }))
J is Relation-like T -defined { the non empty TopSpace-like TopStruct } -valued Function-like constant total quasi_total Element of K19(K20(T,{ the non empty TopSpace-like TopStruct }))
PP is set
rng J is set
rng J is Element of K19({ the non empty TopSpace-like TopStruct })
K19({ the non empty TopSpace-like TopStruct }) is non empty set
PP is 1-sorted
rng J is set
rng J is Element of K19({ the non empty TopSpace-like TopStruct })
K19({ the non empty TopSpace-like TopStruct }) is non empty set
T is non empty set
M is Relation-like T -defined Function-like total 1-sorted-yielding () set
J is Element of T
M . J is set
dom M is Element of K19(T)
K19(T) is non empty set
M . J is 1-sorted
rng M is set
T is set
M is Relation-like T -defined Function-like total 1-sorted-yielding () set
Carrier M is Relation-like T -defined Function-like total set
product (Carrier M) is functional with_common_domain product-like set
K19((product (Carrier M))) is non empty set
K19(K19((product (Carrier M)))) is non empty set
J is Element of K19(K19((product (Carrier M))))
PP is Element of K19(K19((product (Carrier M))))
f is set
f is with_common_domain Element of K19((product (Carrier M)))
W is TopStruct
the carrier of W is set
K19( the carrier of W) is non empty set
V is set
Q is Element of K19( the carrier of W)
M . V is set
(Carrier M) +* (V,Q) is Relation-like Function-like set
product ((Carrier M) +* (V,Q)) is functional with_common_domain product-like set
f is set
f is with_common_domain Element of K19((product (Carrier M)))
W is TopStruct
the carrier of W is set
K19( the carrier of W) is non empty set
V is set
Q is Element of K19( the carrier of W)
M . V is set
(Carrier M) +* (V,Q) is Relation-like Function-like set
product ((Carrier M) +* (V,Q)) is functional with_common_domain product-like set
T is set
K19(T) is non empty set
K19(K19(T)) is non empty set
M is Element of K19(K19(T))
FinMeetCl M is Element of K19(K19(T))
UniCl (FinMeetCl M) is Element of K19(K19(T))
TopStruct(# T,(UniCl (FinMeetCl M)) #) is strict TopStruct
the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #) is set
the topology of TopStruct(# T,(UniCl (FinMeetCl M)) #) is Element of K19(K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #)))
K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #)) is non empty set
K19(K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #))) is non empty set
PP is Element of K19(K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #)))
union PP is Element of K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #))
PP is Element of K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #))
f is Element of K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #))
PP /\ f is Element of K19( the carrier of TopStruct(# T,(UniCl (FinMeetCl M)) #))
T is set
M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set
Carrier M is Relation-like T -defined Function-like total set
product (Carrier M) is functional with_common_domain product-like set
(T,M) is Element of K19(K19((product (Carrier M))))
K19((product (Carrier M))) is non empty set
K19(K19((product (Carrier M)))) is non empty set
PP is Element of K19(K19((product (Carrier M))))
FinMeetCl PP is Element of K19(K19((product (Carrier M))))
UniCl (FinMeetCl PP) is Element of K19(K19((product (Carrier M))))
TopStruct(# (product (Carrier M)),(UniCl (FinMeetCl PP)) #) is strict TopStruct
f is strict TopStruct
f is strict TopSpace-like TopStruct
the carrier of f is set
K19( the carrier of f) is non empty set
K19(K19( the carrier of f)) is non empty set
rng (Carrier M) is set
dom (Carrier M) is Element of K19(T)
K19(T) is non empty set
V is set
(Carrier M) . V is set
M . V is set
W is 1-sorted
the carrier of W is set
dom M is Element of K19(T)
rng M is set
Q is non empty 1-sorted
the carrier of Q is non empty set
J is strict TopSpace-like TopStruct
the carrier of J is set
K19( the carrier of J) is non empty set
K19(K19( the carrier of J)) is non empty set
PP is strict TopSpace-like TopStruct
the carrier of PP is set
K19( the carrier of PP) is non empty set
K19(K19( the carrier of PP)) is non empty set
rng (Carrier M) is set
dom (Carrier M) is Element of K19(T)
K19(T) is non empty set
f is set
(Carrier M) . f is set
M . f is set
f is 1-sorted
the carrier of f is set
dom M is Element of K19(T)
rng M is set
V is non empty 1-sorted
the carrier of V is non empty set
f is non empty TopSpace-like TopStruct
f is non empty TopSpace-like TopStruct
T is set
M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set
(T,M) is strict TopSpace-like TopStruct
Carrier M is Relation-like T -defined Function-like total set
rng (Carrier M) is set
dom (Carrier M) is Element of K19(T)
K19(T) is non empty set
J is set
(Carrier M) . J is set
M . J is set
PP is 1-sorted
the carrier of PP is set
dom M is Element of K19(T)
rng M is set
f is non empty 1-sorted
the carrier of f is non empty set
the carrier of (T,M) is set
product (Carrier M) is functional with_common_domain product-like set
T is non empty set
M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set
J is Element of T
M . J is set
dom M is Element of K19(T)
K19(T) is non empty set
(T,M,J) is TopStruct
rng M is set
T is set
M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set
(T,M) is non empty strict TopSpace-like TopStruct
the carrier of (T,M) is non empty set
Carrier M is Relation-like T -defined Function-like total set
product (Carrier M) is functional with_common_domain product-like set
T is non empty set
M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set
(T,M) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (T,M) is non empty set
J is Relation-like Function-like Element of the carrier of (T,M)
PP is Element of T
J . PP is set
(T,M,PP) is non empty TopStruct
the carrier of (T,M,PP) is non empty set
Carrier M is Relation-like T -defined Function-like total set
dom (Carrier M) is Element of K19(T)
K19(T) is non empty set
(Carrier M) . PP is set
product (Carrier M) is functional with_common_domain product-like set
f is 1-sorted
the carrier of f is set
T is non empty set
M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set
Carrier M is Relation-like T -defined Function-like total set
J is Element of T
proj ((Carrier M),J) is Relation-like product (Carrier M) -defined Function-like total set
product (Carrier M) is functional with_common_domain product-like set
(T,M) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (T,M) is non empty set
(T,M,J) is non empty TopStruct
the carrier of (T,M,J) is non empty set
K20( the carrier of (T,M), the carrier of (T,M,J)) is Relation-like non empty set
K19(K20( the carrier of (T,M), the carrier of (T,M,J))) is non empty set
PP is Relation-like Function-like set
dom PP is set
rng PP is set
f is set
f is set
PP . f is set
V is Relation-like Function-like Element of the carrier of (T,M)
PP . V is set
(T,M,V,J) is Element of the carrier of (T,M,J)
T is non empty set
M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set
(T,M) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (T,M) is non empty set
Carrier M is Relation-like T -defined Function-like total set
J is Element of T
(T,M,J) is non empty TopStruct
the carrier of (T,M,J) is non empty set
K19( the carrier of (T,M,J)) is non empty set
(T,M,J) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,J) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,J)))
K20( the carrier of (T,M), the carrier of (T,M,J)) is Relation-like non empty set
K19(K20( the carrier of (T,M), the carrier of (T,M,J))) is non empty set
proj ((Carrier M),J) is Relation-like product (Carrier M) -defined Function-like total set
product (Carrier M) is functional with_common_domain product-like set
PP is Element of K19( the carrier of (T,M,J))
(T,M,J) " PP is Element of K19( the carrier of (T,M))
K19( the carrier of (T,M)) is non empty set
(Carrier M) +* (J,PP) is Relation-like Function-like set
product ((Carrier M) +* (J,PP)) is functional with_common_domain product-like set
dom (Carrier M) is Element of K19(T)
K19(T) is non empty set
dom ((Carrier M) +* (J,PP)) is set
f is set
V is Relation-like Function-like set
dom V is set
W is set
V . W is set
(Carrier M) . W is set
M . W is set
((Carrier M) +* (J,PP)) . J is set
Q is 1-sorted
the carrier of Q is set
((Carrier M) +* (J,PP)) . W is set
dom (proj ((Carrier M),J)) is with_common_domain Element of K19((product (Carrier M)))
K19((product (Carrier M))) is non empty set
((Carrier M) +* (J,PP)) . J is set
V . J is set
(proj ((Carrier M),J)) . V is set
dom (T,M,J) is non empty Element of K19( the carrier of (T,M))
f is set
dom (proj ((Carrier M),J)) is with_common_domain Element of K19((product (Carrier M)))
K19((product (Carrier M))) is non empty set
V is Relation-like Function-like set
dom V is set
W is set
V . W is set
((Carrier M) +* (J,PP)) . W is set
(Carrier M) . W is set
(proj ((Carrier M),J)) . f is set
V . J is set
T is non empty set
M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set
(T,M) is non empty strict TopSpace-like constituted-Functions TopStruct
J is Element of T
(T,M,J) is non empty TopStruct
(T,M,J) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,J) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,J)))
the carrier of (T,M) is non empty set
the carrier of (T,M,J) is non empty set
K20( the carrier of (T,M), the carrier of (T,M,J)) is Relation-like non empty set
K19(K20( the carrier of (T,M), the carrier of (T,M,J))) is non empty set
Carrier M is Relation-like T -defined Function-like total set
proj ((Carrier M),J) is Relation-like product (Carrier M) -defined Function-like total set
product (Carrier M) is functional with_common_domain product-like set
K19( the carrier of (T,M,J)) is non empty set
PP is Element of K19( the carrier of (T,M,J))
(T,M,J) " PP is Element of K19( the carrier of (T,M))
K19( the carrier of (T,M)) is non empty set
f is set
dom (proj ((Carrier M),J)) is with_common_domain Element of K19((product (Carrier M)))
K19((product (Carrier M))) is non empty set
K19((product (Carrier M))) is non empty set
(T,M) is Element of K19(K19((product (Carrier M))))
K19(K19((product (Carrier M)))) is non empty set
K19(K19( the carrier of (T,M))) is non empty set
the topology of (T,M) is non empty Element of K19(K19( the carrier of (T,M)))
f is with_common_domain Element of K19((product (Carrier M)))
(Carrier M) +* (J,PP) is Relation-like Function-like set
product ((Carrier M) +* (J,PP)) is functional with_common_domain product-like set
[#] (T,M,J) is non empty non proper Element of K19( the carrier of (T,M,J))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
M is non empty set
J is Relation-like M -defined Function-like total 1-sorted-yielding non-Empty () set
(M,J) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (M,J) is non empty set
K20( the carrier of T, the carrier of (M,J)) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of (M,J))) is non empty set
PP is Relation-like the carrier of T -defined the carrier of (M,J) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (M,J)))
(M,J) is Element of K19(K19((product (Carrier J))))
Carrier J is Relation-like M -defined Function-like total set
product (Carrier J) is functional with_common_domain product-like set
K19((product (Carrier J))) is non empty set
K19(K19((product (Carrier J)))) is non empty set
f is Element of M
(M,J,f) is non empty TopStruct
(M,J,f) is Relation-like the carrier of (M,J) -defined the carrier of (M,J,f) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (M,J), the carrier of (M,J,f)))
the carrier of (M,J,f) is non empty set
K20( the carrier of (M,J), the carrier of (M,J,f)) is Relation-like non empty set
K19(K20( the carrier of (M,J), the carrier of (M,J,f))) is non empty set
proj ((Carrier J),f) is Relation-like product (Carrier J) -defined Function-like total set
(M,J,f) * PP is Relation-like the carrier of T -defined the carrier of (M,J,f) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (M,J,f)))
K20( the carrier of T, the carrier of (M,J,f)) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of (M,J,f))) is non empty set
K19( the carrier of (M,J)) is non empty set
f is Element of K19( the carrier of (M,J))
PP " f is Element of K19( the carrier of T)
K19( the carrier of T) is non empty set
V is with_common_domain Element of K19((product (Carrier J)))
Q is TopStruct
the carrier of Q is set
K19( the carrier of Q) is non empty set
W is set
x is Element of K19( the carrier of Q)
J . W is set
(Carrier J) +* (W,x) is Relation-like Function-like set
product ((Carrier J) +* (W,x)) is functional with_common_domain product-like set
Q is Element of M
(M,J,Q) is non empty TopStruct
the carrier of (M,J,Q) is non empty set
K19( the carrier of (M,J,Q)) is non empty set
(M,J,Q) is Relation-like the carrier of (M,J) -defined the carrier of (M,J,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (M,J), the carrier of (M,J,Q)))
K20( the carrier of (M,J), the carrier of (M,J,Q)) is Relation-like non empty set
K19(K20( the carrier of (M,J), the carrier of (M,J,Q))) is non empty set
proj ((Carrier J),Q) is Relation-like product (Carrier J) -defined Function-like total set
(M,J,Q) * PP is Relation-like the carrier of T -defined the carrier of (M,J,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (M,J,Q)))
K20( the carrier of T, the carrier of (M,J,Q)) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of (M,J,Q))) is non empty set
[#] (M,J,Q) is non empty non proper Element of K19( the carrier of (M,J,Q))
v is Element of K19( the carrier of (M,J,Q))
((M,J,Q) * PP) " v is Element of K19( the carrier of T)
(M,J,Q) " v is Element of K19( the carrier of (M,J))
K19(K19( the carrier of (M,J))) is non empty set
T is non empty set
M is Relation-like T -defined Function-like total 1-sorted-yielding non-Empty () set
(T,M) is non empty strict TopSpace-like constituted-Functions TopStruct
(T,M) is Element of K19(K19((product (Carrier M))))
Carrier M is Relation-like T -defined Function-like total set
product (Carrier M) is functional with_common_domain product-like set
K19((product (Carrier M))) is non empty set
K19(K19((product (Carrier M)))) is non empty set
PP is non empty TopSpace-like TopStruct
the carrier of PP is non empty set
the carrier of (T,M) is non empty set
K20( the carrier of PP, the carrier of (T,M)) is Relation-like non empty set
K19(K20( the carrier of PP, the carrier of (T,M))) is non empty set
f is Relation-like the carrier of PP -defined the carrier of (T,M) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M)))
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K20( the carrier of f, the carrier of (T,M)) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of (T,M))) is non empty set
V is set
W is Element of T
(T,M,W) is non empty TopStruct
the carrier of (T,M,W) is non empty set
(T,M,W) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,W)))
K20( the carrier of (T,M), the carrier of (T,M,W)) is Relation-like non empty set
K19(K20( the carrier of (T,M), the carrier of (T,M,W))) is non empty set
proj ((Carrier M),W) is Relation-like product (Carrier M) -defined Function-like total set
(T,M,W) * f is Relation-like the carrier of PP -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,W)))
K20( the carrier of PP, the carrier of (T,M,W)) is Relation-like non empty set
K19(K20( the carrier of PP, the carrier of (T,M,W))) is non empty set
K20( the carrier of f, the carrier of (T,M,W)) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of (T,M,W))) is non empty set
Q is Relation-like the carrier of f -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,W)))
Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,W) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,W)))
V is Relation-like Function-like set
dom V is set
<:V:> is Relation-like Function-like set
dom <:V:> is set
W is set
Q is set
rng V is set
x is Relation-like Function-like set
dom x is set
Q is set
V . Q is set
v is Element of T
(T,M,v) is non empty TopStruct
the carrier of (T,M,v) is non empty set
K20( the carrier of f, the carrier of (T,M,v)) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of (T,M,v))) is non empty set
W is Relation-like the carrier of f -defined the carrier of (T,M,v) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,v)))
W | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,v) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,v)))
(T,M,v) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,v) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,v)))
K20( the carrier of (T,M), the carrier of (T,M,v)) is Relation-like non empty set
K19(K20( the carrier of (T,M), the carrier of (T,M,v))) is non empty set
proj ((Carrier M),v) is Relation-like product (Carrier M) -defined Function-like total set
(T,M,v) * f is Relation-like the carrier of PP -defined the carrier of (T,M,v) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,v)))
K20( the carrier of PP, the carrier of (T,M,v)) is Relation-like non empty set
K19(K20( the carrier of PP, the carrier of (T,M,v))) is non empty set
V . Q is set
x is Element of T
(T,M,x) is non empty TopStruct
the carrier of (T,M,x) is non empty set
K20( the carrier of f, the carrier of (T,M,x)) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of (T,M,x))) is non empty set
(T,M,x) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,x)))
K20( the carrier of (T,M), the carrier of (T,M,x)) is Relation-like non empty set
K19(K20( the carrier of (T,M), the carrier of (T,M,x))) is non empty set
proj ((Carrier M),x) is Relation-like product (Carrier M) -defined Function-like total set
(T,M,x) * f is Relation-like the carrier of PP -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,x)))
K20( the carrier of PP, the carrier of (T,M,x)) is Relation-like non empty set
K19(K20( the carrier of PP, the carrier of (T,M,x))) is non empty set
Q is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
Q is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
W is set
V . W is set
Q is Element of T
(T,M,Q) is non empty TopStruct
the carrier of (T,M,Q) is non empty set
K20( the carrier of f, the carrier of (T,M,Q)) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of (T,M,Q))) is non empty set
x is Relation-like the carrier of f -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))
x | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,Q) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))
(T,M,Q) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,Q)))
K20( the carrier of (T,M), the carrier of (T,M,Q)) is Relation-like non empty set
K19(K20( the carrier of (T,M), the carrier of (T,M,Q))) is non empty set
proj ((Carrier M),Q) is Relation-like product (Carrier M) -defined Function-like total set
(T,M,Q) * f is Relation-like the carrier of PP -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,Q)))
K20( the carrier of PP, the carrier of (T,M,Q)) is Relation-like non empty set
K19(K20( the carrier of PP, the carrier of (T,M,Q))) is non empty set
rngs V is Relation-like Function-like set
product (rngs V) is functional with_common_domain product-like set
W is set
dom (rngs V) is set
Q is Relation-like Function-like set
dom Q is set
dom (Carrier M) is Element of K19(T)
K19(T) is non empty set
x is set
Q . x is set
(Carrier M) . x is set
V . x is set
Q is Element of T
(T,M,Q) is non empty TopStruct
the carrier of (T,M,Q) is non empty set
K20( the carrier of f, the carrier of (T,M,Q)) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of (T,M,Q))) is non empty set
(T,M,Q) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,Q)))
K20( the carrier of (T,M), the carrier of (T,M,Q)) is Relation-like non empty set
K19(K20( the carrier of (T,M), the carrier of (T,M,Q))) is non empty set
proj ((Carrier M),Q) is Relation-like product (Carrier M) -defined Function-like total set
(T,M,Q) * f is Relation-like the carrier of PP -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,Q)))
K20( the carrier of PP, the carrier of (T,M,Q)) is Relation-like non empty set
K19(K20( the carrier of PP, the carrier of (T,M,Q))) is non empty set
M . x is set
v is Relation-like the carrier of f -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))
v | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,Q) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))
v is Relation-like the carrier of f -defined the carrier of (T,M,Q) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))
v | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,Q) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,Q)))
(rngs V) . x is set
rng v is non empty Element of K19( the carrier of (T,M,Q))
K19( the carrier of (T,M,Q)) is non empty set
W is 1-sorted
the carrier of W is set
W is set
Q is set
V . Q is set
x is Element of T
(T,M,x) is non empty TopStruct
the carrier of (T,M,x) is non empty set
K20( the carrier of f, the carrier of (T,M,x)) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of (T,M,x))) is non empty set
(T,M,x) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,x)))
K20( the carrier of (T,M), the carrier of (T,M,x)) is Relation-like non empty set
K19(K20( the carrier of (T,M), the carrier of (T,M,x))) is non empty set
proj ((Carrier M),x) is Relation-like product (Carrier M) -defined Function-like total set
(T,M,x) * f is Relation-like the carrier of PP -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,x)))
K20( the carrier of PP, the carrier of (T,M,x)) is Relation-like non empty set
K19(K20( the carrier of PP, the carrier of (T,M,x))) is non empty set
Q is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
Q is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
rng V is set
dom Q is non empty Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
rng <:V:> is set
W is Relation-like the carrier of f -defined the carrier of (T,M) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M)))
W | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M)))
dom (W | the carrier of PP) is Element of K19( the carrier of PP)
K19( the carrier of PP) is non empty set
dom W is non empty Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
(dom W) /\ the carrier of PP is Element of K19( the carrier of f)
the carrier of f /\ the carrier of PP is set
dom f is non empty Element of K19( the carrier of PP)
Q is set
(W | the carrier of PP) . Q is set
f . Q is set
rng (W | the carrier of PP) is Element of K19( the carrier of (T,M))
K19( the carrier of (T,M)) is non empty set
dom (Carrier M) is Element of K19(T)
K19(T) is non empty set
x is Relation-like Function-like set
dom x is set
rng f is non empty Element of K19( the carrier of (T,M))
Q is Relation-like Function-like set
dom Q is set
v is set
Q . v is set
x . v is set
V . v is set
W is Element of T
(T,M,W) is non empty TopStruct
the carrier of (T,M,W) is non empty set
K20( the carrier of f, the carrier of (T,M,W)) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of (T,M,W))) is non empty set
(T,M,W) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,W)))
K20( the carrier of (T,M), the carrier of (T,M,W)) is Relation-like non empty set
K19(K20( the carrier of (T,M), the carrier of (T,M,W))) is non empty set
proj ((Carrier M),W) is Relation-like product (Carrier M) -defined Function-like total set
(T,M,W) * f is Relation-like the carrier of PP -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,W)))
K20( the carrier of PP, the carrier of (T,M,W)) is Relation-like non empty set
K19(K20( the carrier of PP, the carrier of (T,M,W))) is non empty set
dom (proj ((Carrier M),W)) is with_common_domain Element of K19((product (Carrier M)))
g is Relation-like the carrier of f -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,W)))
g | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,W) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,W)))
g is Relation-like the carrier of f -defined the carrier of (T,M,W) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,W)))
g | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,W) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,W)))
<:V:> . Q is set
g . Q is set
((T,M,W) * f) . Q is set
(proj ((Carrier M),W)) . Q is set
K19( the carrier of (T,M)) is non empty set
Q is Relation-like the carrier of f -defined the carrier of (T,M) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M)))
x is Element of K19( the carrier of (T,M))
Q " x is Element of K19( the carrier of f)
Q is with_common_domain Element of K19((product (Carrier M)))
W is TopStruct
the carrier of W is set
K19( the carrier of W) is non empty set
v is set
g is Element of K19( the carrier of W)
M . v is set
(Carrier M) +* (v,g) is Relation-like Function-like set
product ((Carrier M) +* (v,g)) is functional with_common_domain product-like set
V . v is set
x is Element of T
(T,M,x) is non empty TopStruct
the carrier of (T,M,x) is non empty set
K20( the carrier of f, the carrier of (T,M,x)) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of (T,M,x))) is non empty set
(T,M,x) is Relation-like the carrier of (T,M) -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M), the carrier of (T,M,x)))
K20( the carrier of (T,M), the carrier of (T,M,x)) is Relation-like non empty set
K19(K20( the carrier of (T,M), the carrier of (T,M,x))) is non empty set
proj ((Carrier M),x) is Relation-like product (Carrier M) -defined Function-like total set
(T,M,x) * f is Relation-like the carrier of PP -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of PP, the carrier of (T,M,x)))
K20( the carrier of PP, the carrier of (T,M,x)) is Relation-like non empty set
K19(K20( the carrier of PP, the carrier of (T,M,x))) is non empty set
K19( the carrier of (T,M,x)) is non empty set
dom (T,M,x) is non empty Element of K19( the carrier of (T,M))
x9 is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
x9 | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
x9 is Relation-like the carrier of f -defined the carrier of (T,M,x) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
x9 | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M,x) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M,x)))
dom x9 is non empty Element of K19( the carrier of f)
dom Q is non empty Element of K19( the carrier of f)
ZZ is Element of K19( the carrier of (T,M,x))
(T,M,x) " ZZ is Element of K19( the carrier of (T,M))
x9 " ZZ is Element of K19( the carrier of f)
ZZ is set
Q . ZZ is set
dom (Carrier M) is Element of K19(T)
K19(T) is non empty set
z is Relation-like Function-like set
dom z is set
(T,M,x) . (Q . ZZ) is set
z . x is set
x9 . ZZ is set
ZZ is set
Q . ZZ is set
rng Q is non empty Element of K19( the carrier of (T,M))
dom (Carrier M) is Element of K19(T)
K19(T) is non empty set
z is Relation-like Function-like set
dom z is set
dom (proj ((Carrier M),x)) is with_common_domain Element of K19((product (Carrier M)))
(T,M,x) . (Q . ZZ) is set
z . x is set
x9 . ZZ is set
[#] (T,M,x) is non empty non proper Element of K19( the carrier of (T,M,x))
Q | the carrier of PP is Relation-like the carrier of PP -defined the carrier of f -defined the carrier of (T,M) -valued Function-like Element of K19(K20( the carrier of f, the carrier of (T,M)))
K19(K19( the carrier of (T,M))) is non empty set
T is non empty TopSpace-like TopStruct
M is non empty TopSpace-like SubSpace of T
incl M is Relation-like the carrier of M -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of T))
the carrier of M is non empty set
the carrier of T is non empty set
K20( the carrier of M, the carrier of T) is Relation-like non empty set
K19(K20( the carrier of M, the carrier of T)) is non empty set
K20( the carrier of T, the carrier of M) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of M)) is non empty set
PP is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total continuous Element of K19(K20( the carrier of T, the carrier of M))
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K20( the carrier of f, the carrier of M) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of M)) is non empty set
f is Relation-like the carrier of f -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of M))
K20( the carrier of f, the carrier of T) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of T)) is non empty set
(incl M) * f is Relation-like the carrier of f -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of T))
W is non empty TopSpace-like TopStruct
the carrier of W is non empty set
K20( the carrier of W, the carrier of M) is Relation-like non empty set
K19(K20( the carrier of W, the carrier of M)) is non empty set
K20( the carrier of W, the carrier of T) is Relation-like non empty set
K19(K20( the carrier of W, the carrier of T)) is non empty set
V is Relation-like the carrier of f -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of T))
Q is Relation-like the carrier of W -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of W, the carrier of T))
Q | the carrier of f is Relation-like the carrier of f -defined the carrier of W -defined the carrier of T -valued Function-like Element of K19(K20( the carrier of W, the carrier of T))
PP * Q is Relation-like the carrier of W -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of W, the carrier of M))
x is Relation-like the carrier of W -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of W, the carrier of M))
x | the carrier of f is Relation-like the carrier of f -defined the carrier of W -defined the carrier of M -valued Function-like Element of K19(K20( the carrier of W, the carrier of M))
dom f is non empty Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
Q is set
f . Q is set
x . Q is set
Q . Q is set
V . Q is set
rng f is non empty Element of K19( the carrier of M)
K19( the carrier of M) is non empty set
v is Element of the carrier of T
(incl M) . v is set
PP . v is Element of the carrier of M
dom x is non empty Element of K19( the carrier of W)
K19( the carrier of W) is non empty set
(dom x) /\ the carrier of f is Element of K19( the carrier of W)
the carrier of W /\ the carrier of f is set
T is 1-sorted
the carrier of T is set
M is TopStruct
the carrier of M is set
K20( the carrier of T, the carrier of M) is Relation-like set
K19(K20( the carrier of T, the carrier of M)) is non empty set
J is Relation-like the carrier of T -defined the carrier of M -valued Function-like quasi_total Element of K19(K20( the carrier of T, the carrier of M))
rng J is Element of K19( the carrier of M)
K19( the carrier of M) is non empty set
M | (rng J) is strict SubSpace of M
T is non empty 1-sorted
the carrier of T is non empty set
M is non empty TopStruct
the carrier of M is non empty set
K20( the carrier of T, the carrier of M) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of M)) is non empty set
J is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))
(T,M,J) is SubSpace of M
rng J is non empty Element of K19( the carrier of M)
K19( the carrier of M) is non empty set
M | (rng J) is non empty strict SubSpace of M
T is 1-sorted
the carrier of T is set
M is TopStruct
the carrier of M is set
K20( the carrier of T, the carrier of M) is Relation-like set
K19(K20( the carrier of T, the carrier of M)) is non empty set
J is Relation-like the carrier of T -defined the carrier of M -valued Function-like quasi_total Element of K19(K20( the carrier of T, the carrier of M))
(T,M,J) is SubSpace of M
rng J is Element of K19( the carrier of M)
K19( the carrier of M) is non empty set
M | (rng J) is strict SubSpace of M
the carrier of (T,M,J) is set
[#] (M | (rng J)) is non proper Element of K19( the carrier of (M | (rng J)))
the carrier of (M | (rng J)) is set
K19( the carrier of (M | (rng J))) is non empty set
T is 1-sorted
the carrier of T is set
M is non empty TopStruct
the carrier of M is non empty set
K20( the carrier of T, the carrier of M) is Relation-like set
K19(K20( the carrier of T, the carrier of M)) is non empty set
J is Relation-like the carrier of T -defined the carrier of M -valued Function-like total quasi_total Element of K19(K20( the carrier of T, the carrier of M))
(T,M,J) is SubSpace of M
rng J is Element of K19( the carrier of M)
K19( the carrier of M) is non empty set
M | (rng J) is strict SubSpace of M
the carrier of (T,M,J) is set
K20( the carrier of T, the carrier of (T,M,J)) is Relation-like set
K19(K20( the carrier of T, the carrier of (T,M,J))) is non empty set
dom J is Element of K19( the carrier of T)
K19( the carrier of T) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
K20( the carrier of T, the carrier of M) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of M)) is non empty set
J is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))
(T,M,J) is non empty TopSpace-like SubSpace of M
rng J is non empty Element of K19( the carrier of M)
K19( the carrier of M) is non empty set
M | (rng J) is non empty strict TopSpace-like SubSpace of M
(T,M,J) is Relation-like the carrier of T -defined the carrier of (T,M,J) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (T,M,J)))
the carrier of (T,M,J) is non empty set
K20( the carrier of T, the carrier of (T,M,J)) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of (T,M,J))) is non empty set
dom J is non empty Element of K19( the carrier of T)
K19( the carrier of T) is non empty set
K20((dom J),(rng J)) is Relation-like non empty set
K19(K20((dom J),(rng J))) is non empty set
[#] M is non empty non proper closed Element of K19( the carrier of M)
K19( the carrier of (T,M,J)) is non empty set
[#] (T,M,J) is non empty non proper closed Element of K19( the carrier of (T,M,J))
J " ([#] (T,M,J)) is Element of K19( the carrier of T)
the topology of T is non empty Element of K19(K19( the carrier of T))
K19(K19( the carrier of T)) is non empty set
PP is Element of K19( the carrier of (T,M,J))
(T,M,J) " PP is Element of K19( the carrier of T)
the topology of (T,M,J) is non empty Element of K19(K19( the carrier of (T,M,J)))
K19(K19( the carrier of (T,M,J))) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
f is Element of K19( the carrier of M)
f /\ ([#] (T,M,J)) is Element of K19( the carrier of (T,M,J))
f is Element of K19( the carrier of M)
J " f is Element of K19( the carrier of T)
(J " f) /\ (J " ([#] (T,M,J))) is Element of K19( the carrier of T)
f /\ ([#] (T,M,J)) is Element of K19( the carrier of (T,M,J))
J " (f /\ ([#] (T,M,J))) is Element of K19( the carrier of T)
[#] (T,M,J) is non empty non proper closed Element of K19( the carrier of (T,M,J))
T is 1-sorted
the carrier of T is set
M is non empty TopStruct
the carrier of M is non empty set
K20( the carrier of T, the carrier of M) is Relation-like set
K19(K20( the carrier of T, the carrier of M)) is non empty set
J is Relation-like the carrier of T -defined the carrier of M -valued Function-like total quasi_total Element of K19(K20( the carrier of T, the carrier of M))
(T,M,J) is SubSpace of M
rng J is Element of K19( the carrier of M)
K19( the carrier of M) is non empty set
M | (rng J) is strict SubSpace of M
the carrier of (T,M,J) is set
(T,M,J) is Relation-like the carrier of T -defined the carrier of (T,M,J) -valued Function-like quasi_total Element of K19(K20( the carrier of T, the carrier of (T,M,J)))
K20( the carrier of T, the carrier of (T,M,J)) is Relation-like set
K19(K20( the carrier of T, the carrier of (T,M,J))) is non empty set
rng (T,M,J) is Element of K19( the carrier of (T,M,J))
K19( the carrier of (T,M,J)) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
K20( the carrier of T, the carrier of M) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of M)) is non empty set
J is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))
(T,M,J) is non empty TopSpace-like SubSpace of M
rng J is non empty Element of K19( the carrier of M)
K19( the carrier of M) is non empty set
M | (rng J) is non empty strict TopSpace-like SubSpace of M
(T,M,J) is Relation-like the carrier of T -defined the carrier of (T,M,J) -valued Function-like non empty total quasi_total onto Element of K19(K20( the carrier of T, the carrier of (T,M,J)))
the carrier of (T,M,J) is non empty set
K20( the carrier of T, the carrier of (T,M,J)) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of (T,M,J))) is non empty set
K20( the carrier of (T,M,J), the carrier of T) is Relation-like non empty set
K19(K20( the carrier of (T,M,J), the carrier of T)) is non empty set
(T,M,J) " is Relation-like the carrier of (T,M,J) -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M,J), the carrier of T))
PP is Relation-like the carrier of (T,M,J) -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M,J), the carrier of T))
K20( the carrier of M, the carrier of T) is Relation-like non empty set
K19(K20( the carrier of M, the carrier of T)) is non empty set
f is Relation-like the carrier of M -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of T))
f | the carrier of (T,M,J) is Relation-like the carrier of M -defined the carrier of (T,M,J) -defined the carrier of M -defined the carrier of T -valued Function-like Element of K19(K20( the carrier of M, the carrier of T))
f * J is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of T))
K20( the carrier of T, the carrier of T) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of T)) is non empty set
f is set
(f * J) . f is set
dom (T,M,J) is non empty Element of K19( the carrier of T)
K19( the carrier of T) is non empty set
dom J is non empty Element of K19( the carrier of T)
J . f is set
f . (J . f) is set
(T,M,J) . f is set
((T,M,J) ") . ((T,M,J) . f) is set
(T,M,J) " is Relation-like Function-like set
((T,M,J) ") . ((T,M,J) . f) is set
dom (f * J) is non empty Element of K19( the carrier of T)
K19( the carrier of T) is non empty set
id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of T))
K20( the carrier of M, the carrier of M) is Relation-like non empty set
K19(K20( the carrier of M, the carrier of M)) is non empty set
J * f is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of M))
f is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of M))
f * f is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of M))
(M,M,f) is non empty TopSpace-like SubSpace of M
rng f is non empty Element of K19( the carrier of M)
M | (rng f) is non empty strict TopSpace-like SubSpace of M
the carrier of (M,M,f) is non empty set
incl (M,M,f) is Relation-like the carrier of (M,M,f) -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (M,M,f), the carrier of M))
K20( the carrier of (M,M,f), the carrier of M) is Relation-like non empty set
K19(K20( the carrier of (M,M,f), the carrier of M)) is non empty set
f * (incl (M,M,f)) is Relation-like the carrier of (M,M,f) -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (M,M,f), the carrier of T))
K20( the carrier of (M,M,f), the carrier of T) is Relation-like non empty set
K19(K20( the carrier of (M,M,f), the carrier of T)) is non empty set
dom (f * (incl (M,M,f))) is non empty Element of K19( the carrier of (M,M,f))
K19( the carrier of (M,M,f)) is non empty set
[#] (M,M,f) is non empty non proper closed Element of K19( the carrier of (M,M,f))
rng f is non empty Element of K19( the carrier of T)
dom J is non empty Element of K19( the carrier of T)
W is set
dom f is non empty Element of K19( the carrier of M)
Q is set
f . Q is set
dom f is non empty Element of K19( the carrier of M)
f . Q is set
J . (f . Q) is set
W is Element of the carrier of (M,M,f)
(f * (incl (M,M,f))) . W is Element of the carrier of T
Q is Element of the carrier of (M,M,f)
(f * (incl (M,M,f))) . Q is Element of the carrier of T
dom (incl (M,M,f)) is non empty Element of K19( the carrier of (M,M,f))
v is Element of the carrier of (T,M,J)
PP . v is Element of the carrier of T
f . W is set
x is Element of the carrier of M
(incl (M,M,f)) . x is set
f . ((incl (M,M,f)) . x) is set
Q is Element of the carrier of M
(f * (incl (M,M,f))) . Q is set
(incl (M,M,f)) . Q is set
f . ((incl (M,M,f)) . Q) is set
f . Q is set
W is Element of the carrier of (T,M,J)
PP . W is Element of the carrier of T
dom (incl (M,M,f)) is non empty Element of K19( the carrier of (M,M,f))
rng (f * (incl (M,M,f))) is non empty Element of K19( the carrier of T)
[#] T is non empty non proper closed Element of K19( the carrier of T)
W is set
J . W is set
f . (J . W) is set
(J * f) * J is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))
((J * f) * J) . W is set
id T is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of T))
J * (id T) is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))
(J * (id T)) . W is set
dom f is non empty Element of K19( the carrier of M)
(incl (M,M,f)) * J is Relation-like the carrier of T -defined the carrier of M -valued Function-like Element of K19(K20( the carrier of T, the carrier of M))
dom ((incl (M,M,f)) * J) is Element of K19( the carrier of T)
(f * (incl (M,M,f))) . (J . W) is set
(f * (incl (M,M,f))) * J is Relation-like the carrier of T -defined the carrier of T -valued Function-like Element of K19(K20( the carrier of T, the carrier of T))
((f * (incl (M,M,f))) * J) . W is set
f * ((incl (M,M,f)) * J) is Relation-like the carrier of T -defined the carrier of T -valued Function-like Element of K19(K20( the carrier of T, the carrier of T))
(f * ((incl (M,M,f)) * J)) . W is set
((incl (M,M,f)) * J) . W is set
f . (((incl (M,M,f)) * J) . W) is set
Q is Element of the carrier of M
(incl (M,M,f)) . Q is set
f . ((incl (M,M,f)) . Q) is set
f . (J . W) is set
(id T) . W is set
K20( the carrier of (T,M,J), the carrier of M) is Relation-like non empty set
K19(K20( the carrier of (T,M,J), the carrier of M)) is non empty set
incl (T,M,J) is Relation-like the carrier of (T,M,J) -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M,J), the carrier of M))
[#] M is non empty non proper closed Element of K19( the carrier of M)
W is Relation-like the carrier of (T,M,J) -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,M,J), the carrier of M))
W * (T,M,J) is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))
dom (W * (T,M,J)) is non empty Element of K19( the carrier of T)
Q is Element of K19( the carrier of M)
J " Q is Element of K19( the carrier of T)
(W * (T,M,J)) " Q is Element of K19( the carrier of T)
x is set
J . x is set
(W * (T,M,J)) . x is set
W . (J . x) is set
Q is Element of the carrier of M
x is set
J . x is set
(W * (T,M,J)) . x is set
W . (J . x) is set
Q is Element of the carrier of M
(f * (incl (M,M,f))) " is Relation-like the carrier of T -defined the carrier of (M,M,f) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (M,M,f)))
K20( the carrier of T, the carrier of (M,M,f)) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of (M,M,f))) is non empty set
Q is Element of K19( the carrier of (M,M,f))
((f * (incl (M,M,f))) ") " Q is Element of K19( the carrier of T)
(incl (M,M,f)) .: Q is Element of K19( the carrier of M)
x is set
Q is set
(incl (M,M,f)) . Q is set
v is Element of the carrier of M
(incl (M,M,f)) . v is set
x is set
Q is Element of the carrier of M
(incl (M,M,f)) . x is set
(f * (incl (M,M,f))) .: Q is Element of K19( the carrier of T)
f .: Q is Element of K19( the carrier of T)
the topology of (M,M,f) is non empty Element of K19(K19( the carrier of (M,M,f)))
K19(K19( the carrier of (M,M,f))) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
K19(K19( the carrier of M)) is non empty set
x is Element of K19( the carrier of M)
x /\ ([#] (M,M,f)) is Element of K19( the carrier of (M,M,f))
Q is Element of K19( the carrier of M)
J " Q is Element of K19( the carrier of T)
v is set
J . v is set
f . (J . v) is set
id T is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of T))
(id T) . v is set
dom f is non empty Element of K19( the carrier of M)
dom f is non empty Element of K19( the carrier of M)
f . (J . v) is set
J . (f . (J . v)) is set
J . ((id T) . v) is set
v is set
W is set
f . W is set
J . v is set
g is Element of the carrier of (T,M,J)
PP . g is Element of the carrier of T
f . (J . v) is set
(id T) . v is set
x is Element of the carrier of (T,M,J)
PP . x is Element of the carrier of T
(W * (T,M,J)) " Q is Element of K19( the carrier of T)
Q is Element of K19( the carrier of M)
f " Q is Element of K19( the carrier of M)
(W * (T,M,J)) " Q is Element of K19( the carrier of T)
J " Q is Element of K19( the carrier of T)
f " (J " Q) is Element of K19( the carrier of M)
(J * f) * J is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))
((J * f) * J) * f is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of M))
id T is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of T))
J * (id T) is Relation-like the carrier of T -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of M))
(J * (id T)) * f is Relation-like the carrier of M -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of M, the carrier of M))
0 is Relation-like non-empty empty-yielding empty Element of K108()
{0,1} is non empty set
{1} is non empty set
{{},{1},{0,1}} is non empty set
bool {0,1} is non empty Element of K19(K19({0,1}))
K19({0,1}) is non empty set
K19(K19({0,1})) is non empty set
J is set
J is Element of K19(K19({0,1}))
TopStruct(# {0,1},J #) is non empty strict TopStruct
PP is non empty strict TopStruct
the carrier of PP is non empty set
the topology of PP is Element of K19(K19( the carrier of PP))
K19( the carrier of PP) is non empty set
K19(K19( the carrier of PP)) is non empty set
T is strict TopStruct
the carrier of T is set
the topology of T is Element of K19(K19( the carrier of T))
K19( the carrier of T) is non empty set
K19(K19( the carrier of T)) is non empty set
M is strict TopStruct
the carrier of M is set
the topology of M is Element of K19(K19( the carrier of M))
K19( the carrier of M) is non empty set
K19(K19( the carrier of M)) is non empty set
() is strict TopStruct
the carrier of () is set
the topology of () is Element of K19(K19( the carrier of ()))
K19( the carrier of ()) is non empty set
K19(K19( the carrier of ())) is non empty set
M is Element of K19(K19( the carrier of ()))
union M is Element of K19( the carrier of ())
{{1}} is non empty set
{{0,1}} is non empty set
{{},{1}} is non empty set
{} \/ {1} is non empty set
{{1},{0,1}} is non empty set
{1} \/ {0,1} is non empty set
{{},{0,1}} is non empty set
{} \/ {0,1} is non empty set
{{1},{0,1}} is non empty set
{{}} \/ {{1},{0,1}} is non empty set
union {{}} is set
union {{1},{0,1}} is set
(union {{}}) \/ (union {{1},{0,1}}) is set
{} \/ (union {{1},{0,1}}) is set
{1} \/ {0,1} is non empty set
{{1}} is non empty set
{{0,1}} is non empty set
{{},{1}} is non empty set
{{1},{0,1}} is non empty set
{{},{0,1}} is non empty set
M is Element of K19( the carrier of ())
J is Element of K19( the carrier of ())
M /\ J is Element of K19( the carrier of ())
the carrier of () is non empty set
K19( the carrier of ()) is non empty set
J is Element of the carrier of ()
PP is Element of the carrier of ()
the topology of () is non empty Element of K19(K19( the carrier of ()))
K19(K19( the carrier of ())) is non empty set
f is Element of K19( the carrier of ())
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
the carrier of () is non empty set
K20( the carrier of T, the carrier of ()) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of ())) is non empty set
J is Relation-like the carrier of T -defined the carrier of () -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of ()))
[#] () is non empty non proper closed Element of K19( the carrier of ())
K19( the carrier of ()) is non empty set
PP is Element of K19( the carrier of ())
the topology of () is non empty Element of K19(K19( the carrier of ()))
K19(K19( the carrier of ())) is non empty set
J " PP is Element of K19( the carrier of T)
K19( the carrier of T) is non empty set
the topology of T is non empty Element of K19(K19( the carrier of T))
K19(K19( the carrier of T)) is non empty set
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K20( the carrier of f, the carrier of ()) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of ())) is non empty set
K19( the carrier of f) is non empty set
the topology of f is non empty Element of K19(K19( the carrier of f))
K19(K19( the carrier of f)) is non empty set
[#] T is non empty non proper closed Element of K19( the carrier of T)
f is Element of K19( the carrier of f)
f /\ ([#] T) is Element of K19( the carrier of T)
V is Element of K19( the carrier of f)
chi (V, the carrier of f) is Relation-like the carrier of f -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f,{{},1}))
K20( the carrier of f,{{},1}) is Relation-like non empty set
K19(K20( the carrier of f,{{},1})) is non empty set
dom (chi (V, the carrier of f)) is non empty Element of K19( the carrier of f)
dom J is non empty Element of K19( the carrier of T)
Q is Relation-like the carrier of f -defined the carrier of () -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of ()))
x is set
J . x is set
Q . x is set
rng J is non empty Element of K19( the carrier of ())
J " {1} is Element of K19( the carrier of T)
Q | the carrier of T is Relation-like the carrier of T -defined the carrier of f -defined the carrier of () -valued Function-like Element of K19(K20( the carrier of f, the carrier of ()))
x is Element of K19( the carrier of ())
Q " x is Element of K19( the carrier of f)
Q is set
Q . Q is set
Q is set
Q . Q is set
dom Q is non empty Element of K19( the carrier of f)
(dom Q) /\ the carrier of T is Element of K19( the carrier of f)
the carrier of f /\ the carrier of T is set
T is set
M is non empty 1-sorted
T --> M is Relation-like T -defined {M} -valued Function-like constant total quasi_total Element of K19(K20(T,{M}))
{M} is non empty set
K20(T,{M}) is Relation-like set
K19(K20(T,{M})) is non empty set
J is 1-sorted
rng (T --> M) is set
rng (T --> M) is Element of K19({M})
K19({M}) is non empty set
T is set
M is TopStruct
T --> M is Relation-like T -defined {M} -valued Function-like constant total quasi_total Element of K19(K20(T,{M}))
{M} is non empty set
K20(T,{M}) is Relation-like set
K19(K20(T,{M})) is non empty set
J is set
rng (T --> M) is set
rng (T --> M) is Element of K19({M})
K19({M}) is non empty set
T is non empty set
M is non empty antisymmetric RelStr
T --> M is Relation-like T -defined {M} -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty Element of K19(K20(T,{M}))
{M} is non empty set
K20(T,{M}) is Relation-like non empty set
K19(K20(T,{M})) is non empty set
product (T --> M) is non empty strict constituted-Functions RelStr
J is Element of T
(T --> M) . J is non empty RelStr
T is non empty set
M is non empty transitive RelStr
T --> M is Relation-like T -defined {M} -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty Element of K19(K20(T,{M}))
{M} is non empty set
K20(T,{M}) is Relation-like non empty set
K19(K20(T,{M})) is non empty set
product (T --> M) is non empty strict constituted-Functions RelStr
J is Element of T
(T --> M) . J is non empty RelStr
BoolePoset 1 is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete RelStr
the topology of () is non empty Element of K19(K19( the carrier of ()))
the carrier of () is non empty set
K19( the carrier of ()) is non empty set
K19(K19( the carrier of ())) is non empty set
T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott TopAugmentation of BoolePoset 1
the topology of T is non empty Element of K19(K19( the carrier of T))
the carrier of T is non empty set
K19( the carrier of T) is non empty set
K19(K19( the carrier of T)) is non empty set
BooleLatt 1 is non empty V100() V107() V114() complete L10()
LattPOSet (BooleLatt 1) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete RelStr
the carrier of (BooleLatt 1) is non empty set
LattRel (BooleLatt 1) is Relation-like the carrier of (BooleLatt 1) -defined the carrier of (BooleLatt 1) -valued total quasi_total V75() V78() V82() Element of K19(K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1)))
K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1)) is Relation-like non empty set
K19(K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1))) is non empty set
RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) is strict RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K19(K20( the carrier of T, the carrier of T))
K20( the carrier of T, the carrier of T) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
the carrier of (LattPOSet (BooleLatt 1)) is non empty set
bool 1 is non empty Element of K19(K19(1))
K19(1) is non empty set
K19(K19(1)) is non empty set
the carrier of (BoolePoset 1) is non empty set
PP is set
f is Element of K19( the carrier of T)
f is Element of the carrier of T
V is Element of the carrier of T
[f,V] is Element of the carrier of [:T,T:]
[:T,T:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,T:] is non empty set
{f,V} is non empty set
{f} is non empty set
{{f,V},{f}} is non empty set
M is Element of the carrier of (BoolePoset 1)
J is Element of the carrier of (BoolePoset 1)
f is non empty directed Element of K19( the carrier of T)
sup f is Element of the carrier of T
{0} is non empty set
J is Element of the carrier of (BoolePoset 1)
{J} is non empty Element of K19( the carrier of (BoolePoset 1))
K19( the carrier of (BoolePoset 1)) is non empty set
sup {J} is Element of the carrier of (BoolePoset 1)
J is Element of the carrier of (BoolePoset 1)
{J} is non empty Element of K19( the carrier of (BoolePoset 1))
K19( the carrier of (BoolePoset 1)) is non empty set
PP is Element of K19( the carrier of T)
V is set
W is Element of K19( the carrier of T)
{0} is non empty set
T is non empty set
T --> () is Relation-like T -defined {()} -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty () Element of K19(K20(T,{()}))
{()} is non empty set
K20(T,{()}) is Relation-like non empty set
K19(K20(T,{()})) is non empty set
Carrier (T --> ()) is Relation-like T -defined Function-like total set
{ (product ((Carrier (T --> ())) +* (b₁,{1}))) where b₁ is Element of T : verum } is set
(T,(T --> ())) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (T,(T --> ())) is non empty set
K19( the carrier of (T,(T --> ()))) is non empty set
K19(K19( the carrier of (T,(T --> ())))) is non empty set
(T,(T --> ())) is Element of K19(K19((product (Carrier (T --> ())))))
product (Carrier (T --> ())) is functional with_common_domain product-like set
K19((product (Carrier (T --> ())))) is non empty set
K19(K19((product (Carrier (T --> ()))))) is non empty set
the topology of (T,(T --> ())) is non empty Element of K19(K19( the carrier of (T,(T --> ()))))
bool the carrier of (T,(T --> ())) is non empty Element of K19(K19( the carrier of (T,(T --> ()))))
f is set
f is Element of T
(Carrier (T --> ())) +* (f,{1}) is Relation-like Function-like set
product ((Carrier (T --> ())) +* (f,{1})) is functional with_common_domain product-like set
V is set
dom ((Carrier (T --> ())) +* (f,{1})) is set
W is Relation-like Function-like set
dom W is set
dom (Carrier (T --> ())) is Element of K19(T)
K19(T) is non empty set
Q is set
W . Q is set
(Carrier (T --> ())) . Q is set
(T --> ()) . Q is set
x is 1-sorted
the carrier of x is set
((Carrier (T --> ())) +* (f,{1})) . Q is set
f is Element of K19(K19( the carrier of (T,(T --> ()))))
f is Element of K19(K19( the carrier of (T,(T --> ()))))
W is set
Q is Element of T
(Carrier (T --> ())) +* (Q,{1}) is Relation-like Function-like set
product ((Carrier (T --> ())) +* (Q,{1})) is functional with_common_domain product-like set
V is Element of K19( the carrier of ())
(T,(T --> ()),Q) is non empty TopStruct
x is with_common_domain Element of K19((product (Carrier (T --> ()))))
(Carrier (T --> ())) +* (Q,V) is Relation-like Function-like set
product ((Carrier (T --> ())) +* (Q,V)) is functional with_common_domain product-like set
V is Element of K19(K19( the carrier of (T,(T --> ()))))
W is Element of K19(K19( the carrier of (T,(T --> ()))))
FinMeetCl W is Element of K19(K19( the carrier of (T,(T --> ()))))
(FinMeetCl W) \ {{}} is Element of K19(K19( the carrier of (T,(T --> ()))))
Q is open quasi_basis Element of K19(K19( the carrier of (T,(T --> ()))))
FinMeetCl f is Element of K19(K19( the carrier of (T,(T --> ()))))
x is set
Q is Element of K19( the carrier of (T,(T --> ())))
v is Element of K19(K19( the carrier of (T,(T --> ()))))
Intersect v is Element of K19( the carrier of (T,(T --> ())))
v /\ f is Element of K19(K19( the carrier of (T,(T --> ()))))
W is Element of K19(K19( the carrier of (T,(T --> ()))))
Intersect W is Element of K19( the carrier of (T,(T --> ())))
g is set
x is set
ZZ is with_common_domain Element of K19((product (Carrier (T --> ()))))
ZZ is TopStruct
the carrier of ZZ is set
K19( the carrier of ZZ) is non empty set
x9 is set
z is Element of K19( the carrier of ZZ)
(T --> ()) . x9 is set
(Carrier (T --> ())) +* (x9,z) is Relation-like Function-like set
product ((Carrier (T --> ())) +* (x9,z)) is functional with_common_domain product-like set
the topology of ZZ is Element of K19(K19( the carrier of ZZ))
K19(K19( the carrier of ZZ)) is non empty set
z9 is Element of K19( the carrier of ())
dom (Carrier (T --> ())) is Element of K19(T)
K19(T) is non empty set
(Carrier (T --> ())) +* (x9,{}) is Relation-like Function-like set
((Carrier (T --> ())) +* (x9,{})) . x9 is set
dom ((Carrier (T --> ())) +* (x9,{})) is set
rng ((Carrier (T --> ())) +* (x9,{})) is set
(Carrier (T --> ())) . x9 is set
h1 is Element of T
(Carrier (T --> ())) +* (h1,{1}) is Relation-like Function-like set
product ((Carrier (T --> ())) +* (h1,{1})) is functional with_common_domain product-like set
h2 is 1-sorted
the carrier of h2 is set
T is non empty set
M is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete RelStr
T --> M is Relation-like T -defined {M} -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding Element of K19(K20(T,{M}))
{M} is non empty set
K20(T,{M}) is Relation-like non empty set
K19(K20(T,{M})) is non empty set
product (T --> M) is non empty strict reflexive transitive antisymmetric constituted-Functions RelStr
J is Relation-like T -defined Function-like total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding set
PP is Element of T
J . PP is non empty reflexive RelStr
T is non empty set
M is non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete RelStr
T --> M is Relation-like T -defined {M} -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding Element of K19(K20(T,{M}))
{M} is non empty set
K20(T,{M}) is Relation-like non empty set
K19(K20(T,{M})) is non empty set
product (T --> M) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() up-complete /\-complete RelStr
PP is Element of T
(T --> M) . PP is non empty reflexive RelStr
T is non empty set
BoolePoset T is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete RelStr
the carrier of (BoolePoset T) is non empty set
T --> (BoolePoset 1) is Relation-like T -defined {(BoolePoset 1)} -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding Element of K19(K20(T,{(BoolePoset 1)}))
{(BoolePoset 1)} is non empty set
K20(T,{(BoolePoset 1)}) is Relation-like non empty set
K19(K20(T,{(BoolePoset 1)})) is non empty set
product (T --> (BoolePoset 1)) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete RelStr
the carrier of (product (T --> (BoolePoset 1))) is non empty set
K20( the carrier of (BoolePoset T), the carrier of (product (T --> (BoolePoset 1)))) is Relation-like non empty set
K19(K20( the carrier of (BoolePoset T), the carrier of (product (T --> (BoolePoset 1))))) is non empty set
K19(T) is non empty set
K20(T,{{},1}) is Relation-like non empty set
K19(K20(T,{{},1})) is non empty set
bool T is non empty Element of K19(K19(T))
K19(K19(T)) is non empty set
J is Relation-like Function-like set
dom J is set
BooleLatt 1 is non empty V100() V107() V114() complete L10()
LattPOSet (BooleLatt 1) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete RelStr
the carrier of (BooleLatt 1) is non empty set
LattRel (BooleLatt 1) is Relation-like the carrier of (BooleLatt 1) -defined the carrier of (BooleLatt 1) -valued total quasi_total V75() V78() V82() Element of K19(K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1)))
K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1)) is Relation-like non empty set
K19(K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1))) is non empty set
RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) is strict RelStr
the carrier of (BoolePoset 1) is non empty set
bool {{}} is non empty Element of K19(K19({{}}))
K19({{}}) is non empty set
K19(K19({{}})) is non empty set
rng J is set
Carrier (T --> (BoolePoset 1)) is Relation-like T -defined Function-like total set
product (Carrier (T --> (BoolePoset 1))) is functional with_common_domain product-like set
PP is set
f is set
J . f is set
chi (f,T) is Relation-like T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20(T,{{},1}))
dom (chi (f,T)) is non empty Element of K19(T)
dom (Carrier (T --> (BoolePoset 1))) is Element of K19(T)
f is set
(chi (f,T)) . f is set
(Carrier (T --> (BoolePoset 1))) . f is set
(T --> (BoolePoset 1)) . f is set
V is 1-sorted
the carrier of V is set
BooleLatt T is non empty V100() V107() V114() complete L10()
LattPOSet (BooleLatt T) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete RelStr
the carrier of (BooleLatt T) is non empty set
LattRel (BooleLatt T) is Relation-like the carrier of (BooleLatt T) -defined the carrier of (BooleLatt T) -valued total quasi_total V75() V78() V82() Element of K19(K20( the carrier of (BooleLatt T), the carrier of (BooleLatt T)))
K20( the carrier of (BooleLatt T), the carrier of (BooleLatt T)) is Relation-like non empty set
K19(K20( the carrier of (BooleLatt T), the carrier of (BooleLatt T))) is non empty set
RelStr(# the carrier of (BooleLatt T),(LattRel (BooleLatt T)) #) is strict RelStr
PP is Relation-like the carrier of (BoolePoset T) -defined the carrier of (product (T --> (BoolePoset 1))) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (BoolePoset T), the carrier of (product (T --> (BoolePoset 1)))))
f is Element of the carrier of (BoolePoset T)
f is Element of the carrier of (BoolePoset T)
PP . f is Relation-like Function-like Element of the carrier of (product (T --> (BoolePoset 1)))
PP . f is Relation-like Function-like Element of the carrier of (product (T --> (BoolePoset 1)))
chi (f,T) is Relation-like T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20(T,{{},1}))
chi (f,T) is Relation-like T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20(T,{{},1}))
V is set
(T --> (BoolePoset 1)) . V is set
(chi (f,T)) . V is set
(chi (f,T)) . V is set
W is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete RelStr
the carrier of W is non empty set
Q is Element of the carrier of W
x is Element of the carrier of W
Q is Element of the carrier of W
x is Element of the carrier of W
Q is Element of the carrier of W
x is Element of the carrier of W
V is Relation-like Function-like set
W is Relation-like Function-like set
Q is set
(T --> (BoolePoset 1)) . Q is set
V . Q is set
W . Q is set
x is RelStr
the carrier of x is set
Q is Element of the carrier of x
v is Element of the carrier of x
W is Element of the carrier of (BoolePoset 1)
g is Element of the carrier of (BoolePoset 1)
(chi (f,T)) . Q is set
(chi (f,T)) . Q is set
rng PP is non empty Element of K19( the carrier of (product (T --> (BoolePoset 1))))
K19( the carrier of (product (T --> (BoolePoset 1)))) is non empty set
f is set
dom (Carrier (T --> (BoolePoset 1))) is Element of K19(T)
f is Relation-like Function-like set
dom f is set
f " {1} is set
W is set
chi ((f " {1}),T) is Relation-like T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20(T,{{},1}))
dom (chi ((f " {1}),T)) is non empty Element of K19(T)
W is set
(chi ((f " {1}),T)) . W is set
f . W is set
(Carrier (T --> (BoolePoset 1))) . W is set
(T --> (BoolePoset 1)) . W is set
Q is 1-sorted
the carrier of Q is set
PP . (f " {1}) is set
f is Element of the carrier of (BoolePoset T)
PP . f is Relation-like Function-like Element of the carrier of (product (T --> (BoolePoset 1)))
f is Element of the carrier of (BoolePoset T)
PP . f is Relation-like Function-like Element of the carrier of (product (T --> (BoolePoset 1)))
chi (f,T) is Relation-like T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20(T,{{},1}))
chi (f,T) is Relation-like T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20(T,{{},1}))
f is Element of K19(T)
PP . f is set
chi (f,T) is Relation-like T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20(T,{{},1}))
T is non empty set
T --> (BoolePoset 1) is Relation-like T -defined {(BoolePoset 1)} -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding Element of K19(K20(T,{(BoolePoset 1)}))
{(BoolePoset 1)} is non empty set
K20(T,{(BoolePoset 1)}) is Relation-like non empty set
K19(K20(T,{(BoolePoset 1)})) is non empty set
product (T --> (BoolePoset 1)) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete RelStr
T --> () is Relation-like T -defined {()} -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty () Element of K19(K20(T,{()}))
{()} is non empty set
K20(T,{()}) is Relation-like non empty set
K19(K20(T,{()})) is non empty set
(T,(T --> ())) is non empty strict TopSpace-like constituted-Functions TopStruct
the topology of (T,(T --> ())) is non empty Element of K19(K19( the carrier of (T,(T --> ()))))
the carrier of (T,(T --> ())) is non empty set
K19( the carrier of (T,(T --> ()))) is non empty set
K19(K19( the carrier of (T,(T --> ())))) is non empty set
the carrier of (product (T --> (BoolePoset 1))) is non empty set
Carrier (T --> (BoolePoset 1)) is Relation-like T -defined Function-like total set
product (Carrier (T --> (BoolePoset 1))) is functional with_common_domain product-like set
BooleLatt 1 is non empty V100() V107() V114() complete L10()
LattPOSet (BooleLatt 1) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete RelStr
the carrier of (BooleLatt 1) is non empty set
LattRel (BooleLatt 1) is Relation-like the carrier of (BooleLatt 1) -defined the carrier of (BooleLatt 1) -valued total quasi_total V75() V78() V82() Element of K19(K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1)))
K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1)) is Relation-like non empty set
K19(K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1))) is non empty set
RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) is strict RelStr
the carrier of (BoolePoset 1) is non empty set
bool {{}} is non empty Element of K19(K19({{}}))
K19({{}}) is non empty set
K19(K19({{}})) is non empty set
dom (Carrier (T --> (BoolePoset 1))) is Element of K19(T)
K19(T) is non empty set
Carrier (T --> ()) is Relation-like T -defined Function-like total set
PP is set
(Carrier (T --> (BoolePoset 1))) . PP is set
(Carrier (T --> ())) . PP is set
(T --> (BoolePoset 1)) . PP is set
f is 1-sorted
the carrier of f is set
(T --> ()) . PP is set
f is 1-sorted
the carrier of f is set
{ (product ((Carrier (T --> ())) +* (b₁,{1}))) where b₁ is Element of T : verum } is set
f is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott TopAugmentation of product (T --> (BoolePoset 1))
the topology of f is non empty Element of K19(K19( the carrier of f))
the carrier of f is non empty set
K19( the carrier of f) is non empty set
K19(K19( the carrier of f)) is non empty set
dom (Carrier (T --> ())) is Element of K19(T)
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued Element of K19(K20( the carrier of f, the carrier of f))
K20( the carrier of f, the carrier of f) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of f)) is non empty set
RelStr(# the carrier of f, the InternalRel of f #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
f is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott TopRelStr
the carrier of f is non empty set
K19( the carrier of f) is non empty set
K19(K19( the carrier of f)) is non empty set
CompactSublatt f is non empty strict reflexive transitive antisymmetric with_suprema full V254(f) M38(f)
the carrier of (CompactSublatt f) is non empty set
{ (uparrow b₁) where b₁ is Element of the carrier of f : b₁ in the carrier of (CompactSublatt f) } is set
V is open quasi_basis Element of K19(K19( the carrier of f))
product (Carrier (T --> ())) is functional with_common_domain product-like set
PP is open quasi_prebasis Element of K19(K19( the carrier of (T,(T --> ()))))
BoolePoset T is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete RelStr
the carrier of (BoolePoset T) is non empty set
K20( the carrier of (BoolePoset T), the carrier of (product (T --> (BoolePoset 1)))) is Relation-like non empty set
K19(K20( the carrier of (BoolePoset T), the carrier of (product (T --> (BoolePoset 1))))) is non empty set
Q is Relation-like the carrier of (BoolePoset T) -defined the carrier of (product (T --> (BoolePoset 1))) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (BoolePoset T), the carrier of (product (T --> (BoolePoset 1)))))
FinMeetCl PP is Element of K19(K19( the carrier of (T,(T --> ()))))
x is set
Q is Relation-like Function-like set
dom Q is set
W is Element of K19(K19( the carrier of (T,(T --> ()))))
Intersect W is Element of K19( the carrier of (T,(T --> ())))
rng Q is set
g is set
x is Element of T
(Carrier (T --> ())) +* (x,{1}) is Relation-like Function-like set
product ((Carrier (T --> ())) +* (x,{1})) is functional with_common_domain product-like set
Q . x is set
g is set
Q .: g is set
x is Element of K19(T)
ZZ is Element of the carrier of (BoolePoset T)
Q . ZZ is Relation-like Function-like Element of the carrier of (product (T --> (BoolePoset 1)))
{ (product ((Carrier (T --> ())) +* (b₁,{1}))) where b₁ is Element of T : b₁ in x } is set
z is set
z9 is set
Q . z9 is set
h1 is Element of T
(Carrier (T --> ())) +* (h1,{1}) is Relation-like Function-like set
product ((Carrier (T --> ())) +* (h1,{1})) is functional with_common_domain product-like set
z is set
z9 is Element of T
(Carrier (T --> ())) +* (z9,{1}) is Relation-like Function-like set
product ((Carrier (T --> ())) +* (z9,{1})) is functional with_common_domain product-like set
Q . z9 is set
x9 is Relation-like Function-like Element of the carrier of (product (T --> (BoolePoset 1)))
uparrow x9 is non empty filtered upper Element of K19( the carrier of (product (T --> (BoolePoset 1))))
K19( the carrier of (product (T --> (BoolePoset 1)))) is non empty set
v is Element of K19( the carrier of (T,(T --> ())))
z is set
z9 is Relation-like Function-like Element of the carrier of (product (T --> (BoolePoset 1)))
h1 is Relation-like Function-like set
h2 is Relation-like Function-like set
chi (ZZ,T) is Relation-like T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20(T,{{},1}))
K20(T,{{},1}) is Relation-like non empty set
K19(K20(T,{{},1})) is non empty set
Z is set
j is Element of T
(Carrier (T --> ())) +* (j,{1}) is Relation-like Function-like set
product ((Carrier (T --> ())) +* (j,{1})) is functional with_common_domain product-like set
(T --> (BoolePoset 1)) . j is non empty reflexive RelStr
h1 . j is set
h2 . j is set
RS is RelStr
the carrier of RS is set
xj is Element of the carrier of RS
yj is Element of the carrier of RS
dom ((Carrier (T --> ())) +* (j,{1})) is set
a is Element of the carrier of (BoolePoset 1)
b is set
h2 . b is set
((Carrier (T --> ())) +* (j,{1})) . b is set
(Carrier (T --> ())) . b is set
w is Relation-like Function-like set
dom w is set
dom h2 is set
b is Relation-like Function-like set
dom b is set
chi (ZZ,T) is Relation-like T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20(T,{{},1}))
K20(T,{{},1}) is Relation-like non empty set
K19(K20(T,{{},1})) is non empty set
z9 is set
h2 is Relation-like Function-like set
dom h2 is set
Z is set
(T --> (BoolePoset 1)) . Z is set
(chi (ZZ,T)) . Z is set
h2 . Z is set
(Carrier (T --> (BoolePoset 1))) . Z is set
RS is 1-sorted
the carrier of RS is set
RS is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete RelStr
the carrier of RS is non empty set
xj is Element of the carrier of RS
yj is Element of the carrier of RS
j is Element of T
(Carrier (T --> ())) +* (j,{1}) is Relation-like Function-like set
((Carrier (T --> ())) +* (j,{1})) . j is set
product ((Carrier (T --> ())) +* (j,{1})) is functional with_common_domain product-like set
dom ((Carrier (T --> ())) +* (j,{1})) is set
a is Relation-like Function-like set
dom a is set
a . j is set
xj is Element of the carrier of RS
yj is Element of the carrier of RS
xj is Element of the carrier of RS
yj is Element of the carrier of RS
h1 is Relation-like Function-like Element of the carrier of (product (T --> (BoolePoset 1)))
z is Element of the carrier of f
uparrow z is non empty filtered upper Element of K19( the carrier of f)
{z} is non empty Element of K19( the carrier of f)
uparrow {z} is non empty upper Element of K19( the carrier of f)
{x9} is non empty with_common_domain Element of K19( the carrier of (product (T --> (BoolePoset 1))))
uparrow {x9} is non empty upper Element of K19( the carrier of (product (T --> (BoolePoset 1))))
rng Q is non empty Element of K19( the carrier of (product (T --> (BoolePoset 1))))
K19( the carrier of (product (T --> (BoolePoset 1)))) is non empty set
x is set
Q is Element of the carrier of f
uparrow Q is non empty filtered upper Element of K19( the carrier of f)
dom Q is non empty Element of K19( the carrier of (BoolePoset T))
K19( the carrier of (BoolePoset T)) is non empty set
W is Relation-like Function-like Element of the carrier of (product (T --> (BoolePoset 1)))
g is set
Q . g is set
x is Element of the carrier of (BoolePoset T)
{ H₁(b₁) where b₁ is Element of T : b₁ in x } is set
{ (product ((Carrier (T --> ())) +* (b₁,{1}))) where b₁ is Element of T : b₁ in x } is set
ZZ is set
x9 is Element of K19(T)
z is Element of T
(Carrier (T --> ())) +* (z,{1}) is Relation-like Function-like set
product ((Carrier (T --> ())) +* (z,{1})) is functional with_common_domain product-like set
{Q} is non empty Element of K19( the carrier of f)
uparrow {Q} is non empty upper Element of K19( the carrier of f)
{W} is non empty with_common_domain Element of K19( the carrier of (product (T --> (BoolePoset 1))))
uparrow {W} is non empty upper Element of K19( the carrier of (product (T --> (BoolePoset 1))))
uparrow W is non empty filtered upper Element of K19( the carrier of (product (T --> (BoolePoset 1))))
ZZ is Element of K19(K19( the carrier of (T,(T --> ()))))
Intersect ZZ is Element of K19( the carrier of (T,(T --> ())))
v is Element of K19( the carrier of (T,(T --> ())))
chi (x,T) is Relation-like T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20(T,{{},1}))
K20(T,{{},1}) is Relation-like non empty set
K19(K20(T,{{},1})) is non empty set
z9 is set
h2 is Relation-like Function-like set
dom h2 is set
Z is set
(T --> (BoolePoset 1)) . Z is set
(chi (x,T)) . Z is set
h2 . Z is set
(Carrier (T --> (BoolePoset 1))) . Z is set
RS is 1-sorted
the carrier of RS is set
RS is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete RelStr
the carrier of RS is non empty set
xj is Element of the carrier of RS
yj is Element of the carrier of RS
j is Element of T
(Carrier (T --> ())) +* (j,{1}) is Relation-like Function-like set
((Carrier (T --> ())) +* (j,{1})) . j is set
product ((Carrier (T --> ())) +* (j,{1})) is functional with_common_domain product-like set
dom ((Carrier (T --> ())) +* (j,{1})) is set
a is Relation-like Function-like set
dom a is set
a . j is set
xj is Element of the carrier of RS
yj is Element of the carrier of RS
xj is Element of the carrier of RS
yj is Element of the carrier of RS
x9 is Element of K19(T)
Q . x9 is set
h1 is Relation-like Function-like Element of the carrier of (product (T --> (BoolePoset 1)))
z is set
z9 is Relation-like Function-like Element of the carrier of (product (T --> (BoolePoset 1)))
h1 is Relation-like Function-like set
h2 is Relation-like Function-like set
x9 is Element of K19(T)
Q . x9 is set
chi (x,T) is Relation-like T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20(T,{{},1}))
K20(T,{{},1}) is Relation-like non empty set
K19(K20(T,{{},1})) is non empty set
Z is set
j is Element of T
(Carrier (T --> ())) +* (j,{1}) is Relation-like Function-like set
product ((Carrier (T --> ())) +* (j,{1})) is functional with_common_domain product-like set
(T --> (BoolePoset 1)) . j is non empty reflexive RelStr
h1 . j is set
h2 . j is set
RS is RelStr
the carrier of RS is set
xj is Element of the carrier of RS
yj is Element of the carrier of RS
a is Element of the carrier of (BoolePoset 1)
b is Element of the carrier of (BoolePoset 1)
dom ((Carrier (T --> ())) +* (j,{1})) is set
w is set
h2 . w is set
((Carrier (T --> ())) +* (j,{1})) . w is set
(Carrier (T --> ())) . w is set
c₃₁ is Relation-like Function-like set
dom c₃₁ is set
dom h2 is set
w is Relation-like Function-like set
dom w is set
W is Element of K19(K19( the carrier of f))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
M is non empty TopSpace-like TopStruct
the carrier of M is non empty set
the topology of T is non empty Element of K19(K19( the carrier of T))
K19( the carrier of T) is non empty set
K19(K19( the carrier of T)) is non empty set
the topology of M is non empty Element of K19(K19( the carrier of M))
K19( the carrier of M) is non empty set
K19(K19( the carrier of M)) is non empty set
J is non empty TopSpace-like TopStruct
the carrier of J is non empty set
K20( the carrier of J, the carrier of M) is Relation-like non empty set
K19(K20( the carrier of J, the carrier of M)) is non empty set
PP is Relation-like the carrier of J -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of J, the carrier of M))
K20( the carrier of J, the carrier of T) is Relation-like non empty set
K19(K20( the carrier of J, the carrier of T)) is non empty set
[#] M is non empty non proper closed Element of K19( the carrier of M)
f is Relation-like the carrier of J -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of J, the carrier of T))
f is Element of K19( the carrier of T)
f " f is Element of K19( the carrier of J)
K19( the carrier of J) is non empty set
V is Element of K19( the carrier of M)
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K20( the carrier of f, the carrier of M) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of M)) is non empty set
[#] T is non empty non proper closed Element of K19( the carrier of T)
K20( the carrier of f, the carrier of T) is Relation-like non empty set
K19(K20( the carrier of f, the carrier of T)) is non empty set
V is Relation-like the carrier of f -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of T))
V | the carrier of J is Relation-like the carrier of J -defined the carrier of f -defined the carrier of T -valued Function-like Element of K19(K20( the carrier of f, the carrier of T))
W is Relation-like the carrier of f -defined the carrier of M -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of f, the carrier of M))
W | the carrier of J is Relation-like the carrier of J -defined the carrier of f -defined the carrier of M -valued Function-like Element of K19(K20( the carrier of f, the carrier of M))
Q is Element of K19( the carrier of M)
W " Q is Element of K19( the carrier of f)
K19( the carrier of f) is non empty set
x is Element of K19( the carrier of T)
T is non empty set
T --> (BoolePoset 1) is Relation-like T -defined {(BoolePoset 1)} -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding Element of K19(K20(T,{(BoolePoset 1)}))
{(BoolePoset 1)} is non empty set
K20(T,{(BoolePoset 1)}) is Relation-like non empty set
K19(K20(T,{(BoolePoset 1)})) is non empty set
product (T --> (BoolePoset 1)) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete RelStr
M is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott TopAugmentation of product (T --> (BoolePoset 1))
T --> () is Relation-like T -defined {()} -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty () Element of K19(K20(T,{()}))
{()} is non empty set
K20(T,{()}) is Relation-like non empty set
K19(K20(T,{()})) is non empty set
Carrier (T --> (BoolePoset 1)) is Relation-like T -defined Function-like total set
dom (Carrier (T --> (BoolePoset 1))) is Element of K19(T)
K19(T) is non empty set
Carrier (T --> ()) is Relation-like T -defined Function-like total set
dom (Carrier (T --> ())) is Element of K19(T)
the topology of M is non empty Element of K19(K19( the carrier of M))
the carrier of M is non empty set
K19( the carrier of M) is non empty set
K19(K19( the carrier of M)) is non empty set
(T,(T --> ())) is non empty strict TopSpace-like constituted-Functions TopStruct
the topology of (T,(T --> ())) is non empty Element of K19(K19( the carrier of (T,(T --> ()))))
the carrier of (T,(T --> ())) is non empty set
K19( the carrier of (T,(T --> ()))) is non empty set
K19(K19( the carrier of (T,(T --> ())))) is non empty set
BooleLatt 1 is non empty V100() V107() V114() complete L10()
LattPOSet (BooleLatt 1) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete RelStr
the carrier of (BooleLatt 1) is non empty set
LattRel (BooleLatt 1) is Relation-like the carrier of (BooleLatt 1) -defined the carrier of (BooleLatt 1) -valued total quasi_total V75() V78() V82() Element of K19(K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1)))
K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1)) is Relation-like non empty set
K19(K20( the carrier of (BooleLatt 1), the carrier of (BooleLatt 1))) is non empty set
RelStr(# the carrier of (BooleLatt 1),(LattRel (BooleLatt 1)) #) is strict RelStr
the carrier of (BoolePoset 1) is non empty set
bool {{}} is non empty Element of K19(K19({{}}))
K19({{}}) is non empty set
K19(K19({{}})) is non empty set
f is set
(Carrier (T --> (BoolePoset 1))) . f is set
(Carrier (T --> ())) . f is set
(T --> (BoolePoset 1)) . f is set
f is 1-sorted
the carrier of f is set
(T --> ()) . f is set
V is 1-sorted
the carrier of V is set
f is Element of T
(T,(T --> ()),f) is non empty TopStruct
the InternalRel of M is Relation-like the carrier of M -defined the carrier of M -valued Element of K19(K20( the carrier of M, the carrier of M))
K20( the carrier of M, the carrier of M) is Relation-like non empty set
K19(K20( the carrier of M, the carrier of M)) is non empty set
RelStr(# the carrier of M, the InternalRel of M #) is non empty strict reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete RelStr
product (Carrier (T --> (BoolePoset 1))) is functional with_common_domain product-like set
product (Carrier (T --> ())) is functional with_common_domain product-like set
T is non empty TopSpace-like T_0 TopStruct
the carrier of T is non empty set
the topology of T is non empty Element of K19(K19( the carrier of T))
K19( the carrier of T) is non empty set
K19(K19( the carrier of T)) is non empty set
InclPoset the topology of T is non empty non trivial strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
M is non empty non trivial set
M --> () is Relation-like M -defined {()} -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty () Element of K19(K20(M,{()}))
{()} is non empty set
K20(M,{()}) is Relation-like non empty set
K19(K20(M,{()})) is non empty set
(M,(M --> ())) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (M,(M --> ())) is non empty set
K20( the carrier of T, the carrier of (M,(M --> ()))) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of (M,(M --> ())))) is non empty set
K19( the carrier of (M,(M --> ()))) is non empty set
K19(K19( the carrier of (M,(M --> ())))) is non empty set
Carrier (M --> ()) is Relation-like M -defined Function-like total set
{ (product ((Carrier (M --> ())) +* (b₁,{1}))) where b₁ is Element of M : verum } is set
{ b₁ where b₁ is Element of K19( the carrier of T) : ( a₁ in b₁ & b₁ is open ) } is set
chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( a₁ in b₁ & b₁ is open ) } , the topology of T) is Relation-like the topology of T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20( the topology of T,{{},1}))
K20( the topology of T,{{},1}) is Relation-like non empty set
K19(K20( the topology of T,{{},1})) is non empty set
f is Relation-like Function-like set
dom f is set
rng f is set
f is set
V is set
f . V is set
{ b₁ where b₁ is Element of K19( the carrier of T) : ( V in b₁ & b₁ is open ) } is set
chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( V in b₁ & b₁ is open ) } , the topology of T) is Relation-like the topology of T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20( the topology of T,{{},1}))
dom (chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( V in b₁ & b₁ is open ) } , the topology of T)) is non empty Element of K19( the topology of T)
K19( the topology of T) is non empty set
dom (Carrier (M --> ())) is Element of K19(M)
K19(M) is non empty set
Q is set
(chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( V in b₁ & b₁ is open ) } , the topology of T)) . Q is set
(Carrier (M --> ())) . Q is set
rng (chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( V in b₁ & b₁ is open ) } , the topology of T)) is non empty Element of K19({{},1})
K19({{},1}) is non empty set
(M --> ()) . Q is set
x is 1-sorted
the carrier of x is set
product (Carrier (M --> ())) is functional with_common_domain product-like set
f is Relation-like the carrier of T -defined the carrier of (M,(M --> ())) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (M,(M --> ()))))
(T,(M,(M --> ())),f) is non empty TopSpace-like SubSpace of (M,(M --> ()))
rng f is non empty Element of K19( the carrier of (M,(M --> ())))
(M,(M --> ())) | (rng f) is non empty strict TopSpace-like SubSpace of (M,(M --> ()))
(T,(M,(M --> ())),f) is Relation-like the carrier of T -defined the carrier of (T,(M,(M --> ())),f) -valued Function-like non empty total quasi_total onto Element of K19(K20( the carrier of T, the carrier of (T,(M,(M --> ())),f)))
the carrier of (T,(M,(M --> ())),f) is non empty set
K20( the carrier of T, the carrier of (T,(M,(M --> ())),f)) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of (T,(M,(M --> ())),f))) is non empty set
rng (T,(M,(M --> ())),f) is non empty Element of K19( the carrier of (T,(M,(M --> ())),f))
K19( the carrier of (T,(M,(M --> ())),f)) is non empty set
[#] (T,(M,(M --> ())),f) is non empty non proper closed Element of K19( the carrier of (T,(M,(M --> ())),f))
PP is open quasi_prebasis Element of K19(K19( the carrier of (M,(M --> ()))))
W is Element of K19( the carrier of (M,(M --> ())))
f " W is Element of K19( the carrier of T)
product (Carrier (M --> ())) is functional with_common_domain product-like set
K19((product (Carrier (M --> ())))) is non empty set
Q is with_common_domain Element of K19((product (Carrier (M --> ()))))
x is Element of M
(Carrier (M --> ())) +* (x,{1}) is Relation-like Function-like set
product ((Carrier (M --> ())) +* (x,{1})) is functional with_common_domain product-like set
dom (Carrier (M --> ())) is Element of K19(M)
K19(M) is non empty set
v is set
{ b₁ where b₁ is Element of K19( the carrier of T) : ( v in b₁ & b₁ is open ) } is set
Q is Element of K19( the carrier of T)
V is Element of K19( the carrier of ())
(Carrier (M --> ())) +* (x,V) is Relation-like Function-like set
dom ((Carrier (M --> ())) +* (x,V)) is set
chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( v in b₁ & b₁ is open ) } , the topology of T) is Relation-like the topology of T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20( the topology of T,{{},1}))
g is set
(chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( v in b₁ & b₁ is open ) } , the topology of T)) . g is set
((Carrier (M --> ())) +* (x,V)) . g is set
dom (chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( v in b₁ & b₁ is open ) } , the topology of T)) is non empty Element of K19( the topology of T)
K19( the topology of T) is non empty set
rng (chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( v in b₁ & b₁ is open ) } , the topology of T)) is non empty Element of K19({{},1})
K19({{},1}) is non empty set
(M --> ()) . g is set
(Carrier (M --> ())) . g is set
x is 1-sorted
the carrier of x is set
dom (chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( v in b₁ & b₁ is open ) } , the topology of T)) is non empty Element of K19( the topology of T)
K19( the topology of T) is non empty set
f . v is set
V is Element of K19( the carrier of ())
(Carrier (M --> ())) +* (x,V) is Relation-like Function-like set
((Carrier (M --> ())) +* (x,V)) . x is set
v is set
{ b₁ where b₁ is Element of K19( the carrier of T) : ( v in b₁ & b₁ is open ) } is set
f . v is set
chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( v in b₁ & b₁ is open ) } , the topology of T) is Relation-like the topology of T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20( the topology of T,{{},1}))
dom ((Carrier (M --> ())) +* (x,V)) is set
g is Relation-like Function-like set
dom g is set
g . x is set
(chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( v in b₁ & b₁ is open ) } , the topology of T)) . x is set
x is Element of K19( the carrier of T)
dom (T,(M,(M --> ())),f) is non empty Element of K19( the carrier of T)
[#] T is non empty non proper closed Element of K19( the carrier of T)
V is Element of the carrier of T
(T,(M,(M --> ())),f) . V is Element of the carrier of (T,(M,(M --> ())),f)
W is Element of the carrier of T
(T,(M,(M --> ())),f) . W is Element of the carrier of (T,(M,(M --> ())),f)
{ b₁ where b₁ is Element of K19( the carrier of T) : ( V in b₁ & b₁ is open ) } is set
{ b₁ where b₁ is Element of K19( the carrier of T) : ( W in b₁ & b₁ is open ) } is set
f . V is Relation-like Function-like Element of the carrier of (M,(M --> ()))
chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( V in b₁ & b₁ is open ) } , the topology of T) is Relation-like the topology of T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20( the topology of T,{{},1}))
f . W is Relation-like Function-like Element of the carrier of (M,(M --> ()))
chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( W in b₁ & b₁ is open ) } , the topology of T) is Relation-like the topology of T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20( the topology of T,{{},1}))
Q is Element of K19( the carrier of T)
v is Element of K19( the carrier of T)
W is Element of K19( the carrier of T)
(chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( V in b₁ & b₁ is open ) } , the topology of T)) . v is set
v is Element of K19( the carrier of T)
W is Element of K19( the carrier of T)
(chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( W in b₁ & b₁ is open ) } , the topology of T)) . v is set
V is Element of K19( the carrier of T)
f .: V is Element of K19( the carrier of (M,(M --> ())))
(Carrier (M --> ())) +* (V,{1}) is Relation-like Function-like set
product ((Carrier (M --> ())) +* (V,{1})) is functional with_common_domain product-like set
(product ((Carrier (M --> ())) +* (V,{1}))) /\ the carrier of (T,(M,(M --> ())),f) is set
W is set
dom f is non empty Element of K19( the carrier of T)
Q is set
f . Q is set
{ b₁ where b₁ is Element of K19( the carrier of T) : ( Q in b₁ & b₁ is open ) } is set
dom ((Carrier (M --> ())) +* (V,{1})) is set
chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( Q in b₁ & b₁ is open ) } , the topology of T) is Relation-like the topology of T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20( the topology of T,{{},1}))
Q is set
(chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( Q in b₁ & b₁ is open ) } , the topology of T)) . Q is set
((Carrier (M --> ())) +* (V,{1})) . Q is set
dom (Carrier (M --> ())) is Element of K19(M)
K19(M) is non empty set
dom (chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( Q in b₁ & b₁ is open ) } , the topology of T)) is non empty Element of K19( the topology of T)
K19( the topology of T) is non empty set
rng (chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( Q in b₁ & b₁ is open ) } , the topology of T)) is non empty Element of K19({{},1})
K19({{},1}) is non empty set
(M --> ()) . Q is set
(Carrier (M --> ())) . Q is set
v is 1-sorted
the carrier of v is set
dom (chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( Q in b₁ & b₁ is open ) } , the topology of T)) is non empty Element of K19( the topology of T)
K19( the topology of T) is non empty set
dom (Carrier (M --> ())) is Element of K19(M)
K19(M) is non empty set
W is set
Q is Relation-like Function-like set
dom Q is set
x is set
f . x is set
Q . V is set
((Carrier (M --> ())) +* (V,{1})) . V is set
{ b₁ where b₁ is Element of K19( the carrier of T) : ( x in b₁ & b₁ is open ) } is set
chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( x in b₁ & b₁ is open ) } , the topology of T) is Relation-like the topology of T -defined {{},1} -valued Function-like non empty total quasi_total Element of K19(K20( the topology of T,{{},1}))
(chi ( { b₁ where b₁ is Element of K19( the carrier of T) : ( x in b₁ & b₁ is open ) } , the topology of T)) . V is set
v is Element of K19( the carrier of T)
(T,(M,(M --> ())),f) " is Relation-like the carrier of (T,(M,(M --> ())),f) -defined the carrier of T -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (T,(M,(M --> ())),f), the carrier of T))
K20( the carrier of (T,(M,(M --> ())),f), the carrier of T) is Relation-like non empty set
K19(K20( the carrier of (T,(M,(M --> ())),f), the carrier of T)) is non empty set
V is Element of K19( the carrier of T)
((T,(M,(M --> ())),f) ") " V is Element of K19( the carrier of (T,(M,(M --> ())),f))
the topology of (M,(M --> ())) is non empty Element of K19(K19( the carrier of (M,(M --> ()))))
W is Element of M
(Carrier (M --> ())) +* (W,{1}) is Relation-like Function-like set
product ((Carrier (M --> ())) +* (W,{1})) is functional with_common_domain product-like set
(Carrier (M --> ())) +* (V,{1}) is Relation-like Function-like set
product ((Carrier (M --> ())) +* (V,{1})) is functional with_common_domain product-like set
(T,(M,(M --> ())),f) .: V is Element of K19( the carrier of (T,(M,(M --> ())),f))
Q is Element of K19( the carrier of (M,(M --> ())))
Q /\ ([#] (T,(M,(M --> ())),f)) is Element of K19( the carrier of (T,(M,(M --> ())),f))
the topology of (T,(M,(M --> ())),f) is non empty Element of K19(K19( the carrier of (T,(M,(M --> ())),f)))
K19(K19( the carrier of (T,(M,(M --> ())),f))) is non empty set
T is non empty TopSpace-like T_0 TopStruct
the carrier of T is non empty set
M is non empty set
M --> () is Relation-like M -defined {()} -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty () Element of K19(K20(M,{()}))
{()} is non empty set
K20(M,{()}) is Relation-like non empty set
K19(K20(M,{()})) is non empty set
(M,(M --> ())) is non empty strict TopSpace-like constituted-Functions TopStruct
the carrier of (M,(M --> ())) is non empty set
K20( the carrier of T, the carrier of (M,(M --> ()))) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of (M,(M --> ())))) is non empty set
J is Relation-like the carrier of T -defined the carrier of (M,(M --> ())) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of T, the carrier of (M,(M --> ()))))
(T,(M,(M --> ())),J) is non empty TopSpace-like SubSpace of (M,(M --> ()))
rng J is non empty Element of K19( the carrier of (M,(M --> ())))
K19( the carrier of (M,(M --> ()))) is non empty set
(M,(M --> ())) | (rng J) is non empty strict TopSpace-like SubSpace of (M,(M --> ()))
(T,(M,(M --> ())),J) is Relation-like the carrier of T -defined the carrier of (T,(M,(M --> ())),J) -valued Function-like non empty total quasi_total onto Element of K19(K20( the carrier of T, the carrier of (T,(M,(M --> ())),J)))
the carrier of (T,(M,(M --> ())),J) is non empty set
K20( the carrier of T, the carrier of (T,(M,(M --> ())),J)) is Relation-like non empty set
K19(K20( the carrier of T, the carrier of (T,(M,(M --> ())),J))) is non empty set