@MISC{PBOOLE.MIZ,
  AUTHOR = {Trybulec, Andrzej},
  TITLE = {Many-sorted Sets},
  SECTION1 = {Preliminaries},
  SECTION2 = {Lattice Properties of Many Sorted Sets},
  SECTION3 = {The Empty Many Sorted Set},
  SECTION4 = {The Difference and the Symmetric Difference},
  SECTION5 = {Meeting and Overlapping},
  SECTION6 = {The Second Inclusion},
  SECTION7 = {Non empty set of sorts},
  SECTION8 = {Non Empty and Non-empty Many Sorted Sets},
  DAY = {07},
  MONTH = {July},
  YEAR = {1993},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = {The article deals with parameterized families of sets. When treated in
a similar way as sets (due to systematic overloading notation used for sets)
they are called many sorted sets. For instance, if $x$ and $X$ are two
many-sorted sets (with the same set of indices $I$) then relation
 $x \in X$ is defined as $\forall_{i \in I} x_i \in X_i$.\par
I was prompted by a remark in a paper by Tarlecki and Wirsing:
 ``Throughout the paper we deal with many-sorted sets, functions,
relations etc. ... We feel free to use any standard set-theoretic notation
without explicit use of indices''  \cite[p.~97]{Tar-Wir1}.
The aim of this work was to check the feasibility of such approach in Mizar.
It works.\par
Let us observe some peculiarities:
 \begin{itemize}
 \item[-]
  empty set (i.e. the many sorted set with empty set of indices) belongs
   to itself (theorem 133),
 \item[-]
  we get two different inclusions
  $X \subseteq Y$ iff $\forall_{i \in I} X_i \subseteq Y_i$ and
  $X \sqsubseteq Y$ iff $\forall_x x \in X \Rightarrow x \in Y$
equivalent only for sets that yield non empty values.
 \end{itemize}
Therefore the care is advised.}}

