Ordered quasi-cartesian situations
Deﬁnition 41 . An ordered quasi-cartesian situation is a quasi-cartesian situation together with a
partial order on each its set of its arguments of each given form.
Deﬁnition 42. An order-p reserving quasi-cartesian function from a quasi-cartesian situ at io n S
0
to a quasi-ca rtesian situation S
1
is a quasi-cartesian function σ such that σx ⊑ σy ⇒ x ⊑ y for
every indexed family A of forms and x, y ∈ {x ∈ X
0
dom A
| ρ
0
◦x = A} \ ZC
0
.
Obvious 43. Every order-preserving quasi-cartesian function is a quas i-cartesian function with
injective aggregatio n.
Remark 4 4. Using the obvious fact above, we can prove again that the considered quasi-cartesian
functions are with injective aggregation using the below proved statements that they are order-
preserving.
Proposition 45. Cross-composition product (for small indexed families of relations) is an order-
preserving quasi-cartesian function from the quasi-cartesian situation S
0
of binary relations to the
quasi-cartesian situation S
1
of pointfree funcoids over posets with least elements equipped with the
usual orderings of these sets.
Proof. We nee d to prove ∀i ∈ n: (f
i
∅ ∧ g
i
∅) ∧
Q
C
f ⊑
Q
C
g ⇒ f ⊑ g for every n-indexed
families f and g of binary relations.
D
Q
(C)
f
E
Q
a =
Q
i∈n
hf
i
ia
i
.
Fix k ∈ n, x ∈ ℧. Let a = ℧
n\{k}
∪ {(k; x)}. Then
*
Y
(C)
f
+
Y
a =
Y
i∈n
hf
i
i℧ if i
k;
hf
k
i{x} if i = k.
and
*
Y
(C)
g
+
Y
a =
Y
i∈n
hg
i
i℧ if i
k;
hg
k
i{x} if i = k.
Taking into account that hf
i
i℧
∅ and hg
i
i℧
∅ for every i ∈n, by properties of Cartesian product,
we get hf
k
i{x} ⊑ hg
k
i{x} for every x ∈ ℧ and thus f
k
⊑ g
k
.
Corollary 46. Cross-composition product (for small indexed families of Rel -morphisms) is an
order-preserving quasi-cartesian function from the quasi-cartesian situation S
0
of Rel- m orphisms
to the quasi-cartesian situation S
1
of pointfree funcoids over posets with least elements.
Theorem 47. Let each A
i
(for i ∈ n where n is s ome index set) is a separable poset with least
element. Then
∀i ∈ n: a
i
0 ∧
Y
FCD
a ⊑
Y
FCD
b ⇒ a ⊑ b.
Proof. Suppose a⊑
b.
Q
A is a separable poset, Thus it exists y
a such that y ≍ b.
We have ∃i ∈ n: y
i
a
i
and ∀i ∈ n: y
i
≍ b
i
.
Take k ∈ n such that y
k
a
k
. We have y
k
≍ b
k
.
Take z
i
=
a
i
if i
k;
y
k
if i = k
for i ∈ n.
11