@MISC{LATSUM_1.MIZ,
  AUTHOR = {Romanowicz, Katarzyna and Grabowski, Adam},
  TITLE = {The Operation of Addition of Relational Structures},
  SECTION1 = {Preliminaries},
  SECTION2 = {The Wro{\'n}ski's Operation},
  SECTION3 = {Properties of the Addition},
  DAY = {24},
  MONTH = {May},
  YEAR = {2004},
  ADDRESS1 = {University of Bia{\l}ystok},
  ADDRESS2 = {University of Bia{\l}ystok},
  SUMMARY = {The article contains the formalization of the addition operator
  on relational structures as defined by A.~Wro{\'n}ski
  \cite{Wronski:1974} (as a generalization of Troelstra's sum
  or Ja{\'s}kowski star addition).
  The ordering relation of $A \otimes B$ is given by
  $$\le_{A\otimes B}\:=\:\le_A\cup \le_B\cup\: (\le_A \circ \le_B),$$
  where the carrier is defined as the set-theoretical union
  of carriers of $A$ and $B$.
  Main part -- Section 3 -- is devoted to the Mizar translation of Theorem 1
  (iv--xiii), p.~66 of \cite{Wronski:1974}.}}

