Volume 10, Number 3 (2002): pdf, ps, dvi.

- Grzegorz Bancerek, Adam Naumowicz.
Preliminaries to Automatic Generation of Mizar Documentation for Circuits,
Formalized Mathematics 10(3), pages 117-133, 2002. MML Identifier: CIRCCMB3

**Summary**: In this paper we introduce technical notions used by a system which automatically generates Mizar documentation for specified circuits. They provide a ready for use elements needed to justify correctness of circuits' construction. We concentrate on the concept of stabilization and analyze one-gate circuits and their combinations.

- Robert Milewski.
Properties of the Upper and Lower Sequence on the Cage,
Formalized Mathematics 10(3), pages 135-143, 2002. MML Identifier: JORDAN15

**Summary**:

- Adam Grabowski.
On the Decompositions of Intervals and Simple Closed Curves,
Formalized Mathematics 10(3), pages 145-151, 2002. MML Identifier: BORSUK_4

**Summary**: The aim of the paper is to show that the only subcontinua of the Jordan curve are arcs, the whole curve, and singletons of its points. Additionally, it has been shown that the only subcontinua of the unit interval $\Bbb I$ are closed intervals.

- Andrzej Trybulec.
On the Minimal Distance Between Sets in Euclidean Space,
Formalized Mathematics 10(3), pages 153-158, 2002. MML Identifier: JORDAN1K

**Summary**: The concept of the minimal distance between two sets in a Euclidean space is introduced and some useful lemmas are proved.

- Yatsuka Nakamura, Andrzej Trybulec.
Sequences of Metric Spaces and an Abstract Intermediate Value Theorem,
Formalized Mathematics 10(3), pages 159-161, 2002. MML Identifier: TOPMETR3

**Summary**: Relations of convergence of real sequences and convergence of metric spaces are investigated. An abstract intermediate value theorem for two closed sets in the range is presented. At the end, it is proven that an arc connecting the west minimal point and the east maximal point in a simple closed curve must be identical to the upper arc or lower arc of the closed curve.

- Andrzej Trybulec, Yatsuka Nakamura.
On the Decomposition of a Simple Closed Curve into Two Arcs,
Formalized Mathematics 10(3), pages 163-167, 2002. MML Identifier: JORDAN16

**Summary**: The purpose of the paper is to prove lemmas needed for the Jordan curve theorem. The main result is that the decomposition of a simple closed curve into two arcs with the ends $p_1, p_2$ is unique in the sense that every arc on the curve with the same ends must be equal to one of them.

- Artur Kornilowicz.
The Ordering of Points on a Curve. Part III,
Formalized Mathematics 10(3), pages 169-171, 2002. MML Identifier: JORDAN17

**Summary**:

- Artur Kornilowicz.
The Ordering of Points on a Curve. Part IV,
Formalized Mathematics 10(3), pages 173-177, 2002. MML Identifier: JORDAN18

**Summary**:

- Josef Urban.
Order Sorted Algebras,
Formalized Mathematics 10(3), pages 179-188, 2002. MML Identifier: OSALG_1

**Summary**: Initial notions for order sorted algebras.

- Josef Urban.
Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras,
Formalized Mathematics 10(3), pages 189-196, 2002. MML Identifier: OSALG_2

**Summary**:

- Josef Urban.
Homomorphisms of Order Sorted Algebras,
Formalized Mathematics 10(3), pages 197-200, 2002. MML Identifier: OSALG_3

**Summary**:

- Josef Urban.
Order Sorted Quotient Algebra,
Formalized Mathematics 10(3), pages 201-210, 2002. MML Identifier: OSALG_4

**Summary**:

- Josef Urban.
Free Order Sorted Universal Algebra,
Formalized Mathematics 10(3), pages 211-225, 2002. MML Identifier: OSAFREE

**Summary**: Free Order Sorted Universal Algebra --- the general construction for any locally directed signatures.