***** Boolean Properties of Sets --- Theorems *****
**** Library Committee* ****
* Association of Mizar Users
MML identifier: XBOOLE_1, version:
The notation and terminology used in this paper have been introduced in the
following articles: \cite{HIDDEN.ABS}, \cite{XBOOLE_0.ABS}, and \cite
{TARSKI.ABS}.
                            **** 1. Main Part ****
In this paper $x$, $A$, $B$, $X$, $X'$, $Y$, $Y'$, $Z$, $V$ denote sets. Now we
state the propositions:
(1)  Modus Barbara:
     If $X \mathrel{{\href{}{\subseteq}}} Y \mathrel{{\href{}{\subseteq}}} Z$,
     then $X \mathrel{{\href{}{\subseteq}}} Z$.
(2)  ${\href{xboole_0.html#func1}{\emptyset}} \mathrel{{\href{}{\subseteq}}}
     X$.
(3)  If $X \mathrel{{\href{}{\subseteq}}} {\href{xboole_0.html#func1}
     {\emptyset}}$, then $X \mathrel{{\href{}{=}}} {\href{xboole_0.html#func1}
     {\emptyset}}$.
(4)  $(X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y)\mathop{{\href
     {xboole_0.html#func2}{\cup}}} Z \mathrel{{\href{}{=}}} X\mathop{{\href
     {xboole_0.html#func2}{\cup}}} (Y\mathop{{\href{xboole_0.html#func2}
     {\cup}}} Z)$.
(5)  $(X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y)\mathop{{\href
     {xboole_0.html#func2}{\cup}}} Z \mathrel{{\href{}{=}}} (X\mathop{{\href
     {xboole_0.html#func2}{\cup}}} Z)\mathop{{\href{xboole_0.html#func2}
     {\cup}}} (Y\mathop{{\href{xboole_0.html#func2}{\cup}}} Z)$.
(6)  $X\mathop{{\href{xboole_0.html#func2}{\cup}}} (X\mathop{{\href
     {xboole_0.html#func2}{\cup}}} Y) \mathrel{{\href{}{=}}} X\mathop{{\href
     {xboole_0.html#func2}{\cup}}} Y$.
(7)  $X \mathrel{{\href{}{\subseteq}}} X\mathop{{\href{xboole_0.html#func2}
     {\cup}}} Y$.
(8)  If $X \mathrel{{\href{}{\subseteq}}} Z$ and $Y \mathrel{{\href{}
     {\subseteq}}} Z$, then $X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y
     \mathrel{{\href{}{\subseteq}}} Z$.
(9)  If $X \mathrel{{\href{}{\subseteq}}} Y$, then $X\mathop{{\href
     {xboole_0.html#func2}{\cup}}} Z \mathrel{{\href{}{\subseteq}}} Y\mathop{
     {\href{xboole_0.html#func2}{\cup}}} Z$.
(10)  If $X \mathrel{{\href{}{\subseteq}}} Y$, then $X \mathrel{{\href{}
      {\subseteq}}} Z\mathop{{\href{xboole_0.html#func2}{\cup}}} Y$.
(11)  If $X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y \mathrel{{\href{}
      {\subseteq}}} Z$, then $X \mathrel{{\href{}{\subseteq}}} Z$.
(12)  If $X \mathrel{{\href{}{\subseteq}}} Y$, then $X\mathop{{\href
      {xboole_0.html#func2}{\cup}}} Y \mathrel{{\href{}{=}}} Y$.
(13)  Suppose $X \mathrel{{\href{}{\subseteq}}} Y$ and $Z \mathrel{{\href{}
      {\subseteq}}} V$. Then $X\mathop{{\href{xboole_0.html#func2}{\cup}}} Z
      \mathrel{{\href{}{\subseteq}}} Y\mathop{{\href{xboole_0.html#func2}
      {\cup}}} V$.
(14)  Suppose $Y \mathrel{{\href{}{\subseteq}}} X$ and $Z \mathrel{{\href{}
      {\subseteq}}} X$ and for every $V$ such that $Y \mathrel{{\href{}
      {\subseteq}}} V$ and $Z \mathrel{{\href{}{\subseteq}}} V$ holds $X
      \mathrel{{\href{}{\subseteq}}} V$. Then $X \mathrel{{\href{}{=}}}
      Y\mathop{{\href{xboole_0.html#func2}{\cup}}} Z$.
(15)  If $X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y \mathrel{{\href{}{=}}}
      {\href{xboole_0.html#func1}{\emptyset}}$, then $X \mathrel{{\href{}{=}}}
      {\href{xboole_0.html#func1}{\emptyset}}$.
(16)  $(X \mathop{{\href{xboole_0.html#func3}{\cap}}} Y) \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Z \mathrel{{\href{}{=}}} X \mathop{{\href
      {xboole_0.html#func3}{\cap}}} (Y \mathop{{\href{xboole_0.html#func3}
      {\cap}}} Z)$.
(17)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} Y \mathrel{{\href{}
      {\subseteq}}} X$.
(18)  If $X \mathrel{{\href{}{\subseteq}}} Y \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Z$, then $X \mathrel{{\href{}{\subseteq}}}
      Y$.
(19)  If $Z \mathrel{{\href{}{\subseteq}}} X$ and $Z \mathrel{{\href{}
      {\subseteq}}} Y$, then $Z \mathrel{{\href{}{\subseteq}}} X \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Y$.
(20)  Suppose $X \mathrel{{\href{}{\subseteq}}} Y$ and $X \mathrel{{\href{}
      {\subseteq}}} Z$ and for every $V$ such that $V \mathrel{{\href{}
      {\subseteq}}} Y$ and $V \mathrel{{\href{}{\subseteq}}} Z$ holds $V
      \mathrel{{\href{}{\subseteq}}} X$. Then $X \mathrel{{\href{}{=}}} Y
      \mathop{{\href{xboole_0.html#func3}{\cap}}} Z$.
(21)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} (X\mathop{{\href
      {xboole_0.html#func2}{\cup}}} Y) \mathrel{{\href{}{=}}} X$.
(22)  $X\mathop{{\href{xboole_0.html#func2}{\cup}}} X \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Y \mathrel{{\href{}{=}}} X$.
(23)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} (Y\mathop{{\href
      {xboole_0.html#func2}{\cup}}} Z) \mathrel{{\href{}{=}}} X \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Y\mathop{{\href{xboole_0.html#func2}
      {\cup}}} X \mathop{{\href{xboole_0.html#func3}{\cap}}} Z$.
(24)  $X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Z \mathrel{{\href{}{=}}} (X\mathop{{\href
      {xboole_0.html#func2}{\cup}}} Y) \mathop{{\href{xboole_0.html#func3}
      {\cap}}} (X\mathop{{\href{xboole_0.html#func2}{\cup}}} Z)$.
(25)  $(X \mathop{{\href{xboole_0.html#func3}{\cap}}} Y\mathop{{\href
      {xboole_0.html#func2}{\cup}}} Y \mathop{{\href{xboole_0.html#func3}
      {\cap}}} Z)\mathop{{\href{xboole_0.html#func2}{\cup}}} Z \mathop{{\href
      {xboole_0.html#func3}{\cap}}} X \mathrel{{\href{}{=}}} ((X\mathop{{\href
      {xboole_0.html#func2}{\cup}}} Y) \mathop{{\href{xboole_0.html#func3}
      {\cap}}} (Y\mathop{{\href{xboole_0.html#func2}{\cup}}} Z)) \mathop{{\href
      {xboole_0.html#func3}{\cap}}} (Z\mathop{{\href{xboole_0.html#func2}
      {\cup}}} X)$.
(26)  If $X \mathrel{{\href{}{\subseteq}}} Y$, then $X \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Z \mathrel{{\href{}{\subseteq}}} Y \mathop{
      {\href{xboole_0.html#func3}{\cap}}} Z$.
(27)  Suppose $X \mathrel{{\href{}{\subseteq}}} Y$ and $Z \mathrel{{\href{}
      {\subseteq}}} V$. Then $X \mathop{{\href{xboole_0.html#func3}{\cap}}} Z
      \mathrel{{\href{}{\subseteq}}} Y \mathop{{\href{xboole_0.html#func3}
      {\cap}}} V$.
(28)  If $X \mathrel{{\href{}{\subseteq}}} Y$, then $X \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Y \mathrel{{\href{}{=}}} X$.
(29)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} Y \mathrel{{\href{}
      {\subseteq}}} X\mathop{{\href{xboole_0.html#func2}{\cup}}} Z$.
(30)  Suppose $X \mathrel{{\href{}{\subseteq}}} Z$. Then $X\mathop{{\href
      {xboole_0.html#func2}{\cup}}} Y \mathop{{\href{xboole_0.html#func3}
      {\cap}}} Z \mathrel{{\href{}{=}}} (X\mathop{{\href{xboole_0.html#func2}
      {\cup}}} Y) \mathop{{\href{xboole_0.html#func3}{\cap}}} Z$.
(31)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} Y\mathop{{\href
      {xboole_0.html#func2}{\cup}}} X \mathop{{\href{xboole_0.html#func3}
      {\cap}}} Z \mathrel{{\href{}{\subseteq}}} Y\mathop{{\href
      {xboole_0.html#func2}{\cup}}} Z$.
(32)  If $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y \mathrel{{\href
      {}{=}}} Y \mathop{{\href{xboole_0.html#func4}{\setminus}}} X$, then $X
      \mathrel{{\href{}{=}}} Y$.
(33)  If $X \mathrel{{\href{}{\subseteq}}} Y$, then $X \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Z \mathrel{{\href{}{\subseteq}}} Y
      \mathop{{\href{xboole_0.html#func4}{\setminus}}} Z$.
(34)  If $X \mathrel{{\href{}{\subseteq}}} Y$, then $Z \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Y \mathrel{{\href{}{\subseteq}}} Z
      \mathop{{\href{xboole_0.html#func4}{\setminus}}} X$.
(35)  Suppose $X \mathrel{{\href{}{\subseteq}}} Y$ and $Z \mathrel{{\href{}
      {\subseteq}}} V$. Then $X \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} V \mathrel{{\href{}{\subseteq}}} Y \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Z$.
(36)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y \mathrel{{\href{}
      {\subseteq}}} X$.
(37)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y \mathrel{{\href{}
      {=}}} {\href{xboole_0.html#func1}{\emptyset}}$ if and only if $X \mathrel
      {{\href{}{\subseteq}}} Y$.
(38)  If $X \mathrel{{\href{}{\subseteq}}} Y \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} X$, then $X \mathrel{{\href{}{=}}}
      {\href{xboole_0.html#func1}{\emptyset}}$.
(39)  $X\mathop{{\href{xboole_0.html#func2}{\cup}}} (Y \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} X) \mathrel{{\href{}{=}}} X\mathop{
      {\href{xboole_0.html#func2}{\cup}}} Y$.
(40)  $(X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y) \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Y \mathrel{{\href{}{=}}} X \mathop{
      {\href{xboole_0.html#func4}{\setminus}}} Y$.
(41)  $(X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y) \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Z \mathrel{{\href{}{=}}} X \mathop{
      {\href{xboole_0.html#func4}{\setminus}}} (Y\mathop{{\href
      {xboole_0.html#func2}{\cup}}} Z)$.
(42)  $(X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y) \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Z \mathrel{{\href{}{=}}} (X \mathop{
      {\href{xboole_0.html#func4}{\setminus}}} Z)\mathop{{\href
      {xboole_0.html#func2}{\cup}}} (Y \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} Z)$.
(43)  If $X \mathrel{{\href{}{\subseteq}}} Y\mathop{{\href{xboole_0.html#func2}
      {\cup}}} Z$, then $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y
      \mathrel{{\href{}{\subseteq}}} Z$.
(44)  If $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y \mathrel{{\href
      {}{\subseteq}}} Z$, then $X \mathrel{{\href{}{\subseteq}}} Y\mathop{
      {\href{xboole_0.html#func2}{\cup}}} Z$.
(45)  If $X \mathrel{{\href{}{\subseteq}}} Y$, then $Y \mathrel{{\href{}{=}}}
      X\mathop{{\href{xboole_0.html#func2}{\cup}}} (Y \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} X)$.
(46)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} (X\mathop{{\href
      {xboole_0.html#func2}{\cup}}} Y) \mathrel{{\href{}{=}}} {\href
      {xboole_0.html#func1}{\emptyset}}$.
(47)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} X \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Y \mathrel{{\href{}{=}}} X \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Y$.
(48)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} (X \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Y) \mathrel{{\href{}{=}}} X \mathop{
      {\href{xboole_0.html#func3}{\cap}}} Y$.
(49)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} (Y \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Z) \mathrel{{\href{}{=}}} X \mathop{
      {\href{xboole_0.html#func3}{\cap}}} Y \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} Z$.
(50)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} (Y \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Z) \mathrel{{\href{}{=}}} X \mathop{
      {\href{xboole_0.html#func3}{\cap}}} Y \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} X \mathop{{\href{xboole_0.html#func3}{\cap}}} Z$.
(51)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} Y\mathop{{\href
      {xboole_0.html#func2}{\cup}}} (X \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} Y) \mathrel{{\href{}{=}}} X$.
(52)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} (Y \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Z) \mathrel{{\href{}{=}}} (X \mathop{
      {\href{xboole_0.html#func4}{\setminus}}} Y)\mathop{{\href
      {xboole_0.html#func2}{\cup}}} X \mathop{{\href{xboole_0.html#func3}
      {\cap}}} Z$.
(53)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} (Y\mathop{{\href
      {xboole_0.html#func2}{\cup}}} Z) \mathrel{{\href{}{=}}} (X \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Y) \mathop{{\href{xboole_0.html#func3}
      {\cap}}} (X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Z)$.
(54)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Z \mathrel{{\href{}{=}}} (X \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Y)\mathop{{\href{xboole_0.html#func2}
      {\cup}}} (X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Z)$.
(55)  $(X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y) \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} X \mathop{{\href{xboole_0.html#func3}
      {\cap}}} Y \mathrel{{\href{}{=}}} (X \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} Y)\mathop{{\href{xboole_0.html#func2}{\cup}}} (Y \mathop{
      {\href{xboole_0.html#func4}{\setminus}}} X)$.
(56)  If $X \mathrel{{\href{}{\subset}}} Y \mathrel{{\href{}{\subset}}} Z$,
      then $X \mathrel{{\href{}{\subset}}} Z$.
(57)  not $X \mathrel{{\href{}{\subset}}} Y \mathrel{{\href{}{\subset}}} X$.
(58)  If $X \mathrel{{\href{}{\subset}}} Y \mathrel{{\href{}{\subseteq}}} Z$,
      then $X \mathrel{{\href{}{\subset}}} Z$.
(59)  If $X \mathrel{{\href{}{\subseteq}}} Y \mathrel{{\href{}{\subset}}} Z$,
      then $X \mathrel{{\href{}{\subset}}} Z$.
(60)  If $X \mathrel{{\href{}{\subseteq}}} Y$, then $Y \mathrel{{\href{}
      {\not\subset}}} X$.
(61)  If $X\mathrel{{\href{}{\neq}}} {\href{xboole_0.html#func1}{\emptyset}}$,
      then ${\href{xboole_0.html#func1}{\emptyset}} \mathrel{{\href{}
      {\subset}}} X$.
(62)  $X \mathrel{{\href{}{\not\subset}}} {\href{xboole_0.html#func1}
      {\emptyset}}$.
Now we state the propositions:
(63)  Modus Darii:
      If $X \mathrel{{\href{}{\subseteq}}} Y$ and $Y$misses$Z$, then
      $X$misses$Z$.
(64)  If $A \mathrel{{\href{}{\subseteq}}} X$ and $B \mathrel{{\href{}
      {\subseteq}}} Y$ and $X$misses$Y$, then $A$misses$B$.
(65)  $X$misses${\href{xboole_0.html#func1}{\emptyset}}$.
(66)  $X$meets$X$ if and only if $X\mathrel{{\href{}{\neq}}} {\href
      {xboole_0.html#func1}{\emptyset}}$.
(67)  If $X \mathrel{{\href{}{\subseteq}}} Y$ and $X \mathrel{{\href{}
      {\subseteq}}} Z$ and $Y$misses$Z$, then $X \mathrel{{\href{}{=}}} {\href
      {xboole_0.html#func1}{\emptyset}}$.
Let us consider non empty set $A$. Now we state the propositions:
(68)  If $A \mathrel{{\href{}{\subseteq}}} Y$ and $A \mathrel{{\href{}
      {\subseteq}}} Z$, then $Y$meets$Z$.
(69)  If $A \mathrel{{\href{}{\subseteq}}} Y$, then $A$meets$Y$.
Now we state the propositions:
(70)  $X$meets$Y\mathop{{\href{xboole_0.html#func2}{\cup}}} Z$ if and only if
      $X$meets$Y$ or $X$meets$Z$.
(71)  If $X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y \mathrel{{\href{}{=}}}
      Z\mathop{{\href{xboole_0.html#func2}{\cup}}} Y$ and $X$misses$Y$ and
      $Z$misses$Y$, then $X \mathrel{{\href{}{=}}} Z$.
(72)  If $X'\mathop{{\href{xboole_0.html#func2}{\cup}}} Y' \mathrel{{\href{}
      {=}}} X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y$ and $X$misses$X'$
      and $Y$misses$Y'$, then $X \mathrel{{\href{}{=}}} Y'$.
(73)  If $X \mathrel{{\href{}{\subseteq}}} Y\mathop{{\href{xboole_0.html#func2}
      {\cup}}} Z$ and $X$misses$Z$, then $X \mathrel{{\href{}{\subseteq}}} Y$.
(74)  If $X$meets$Y \mathop{{\href{xboole_0.html#func3}{\cap}}} Z$, then
      $X$meets$Y$.
(75)  If $X$meets$Y$, then $X \mathop{{\href{xboole_0.html#func3}{\cap}}}
      Y$meets$Y$.
(76)  If $Y$misses$Z$, then $X \mathop{{\href{xboole_0.html#func3}{\cap}}}
      Y$misses$X \mathop{{\href{xboole_0.html#func3}{\cap}}} Z$.
(77)  If $X$meets$Y$ and $X \mathrel{{\href{}{\subseteq}}} Z$, then $X$meets$Y
      \mathop{{\href{xboole_0.html#func3}{\cap}}} Z$.
(78)  If $X$misses$Y$, then $X \mathop{{\href{xboole_0.html#func3}{\cap}}}
      (Y\mathop{{\href{xboole_0.html#func2}{\cup}}} Z) \mathrel{{\href{}{=}}} X
      \mathop{{\href{xboole_0.html#func3}{\cap}}} Z$.
(79)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y$misses$Y$.
(80)  If $X$misses$Y$, then $X$misses$Y \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} Z$.
(81)  If $X$misses$Y \mathop{{\href{xboole_0.html#func4}{\setminus}}} Z$, then
      $Y$misses$X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Z$.
(82)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y$misses$Y \mathop{
      {\href{xboole_0.html#func4}{\setminus}}} X$.
(83)  $X$misses$Y$ if and only if $X \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} Y \mathrel{{\href{}{=}}} X$.
(84)  If $X$meets$Y$ and $X$misses$Z$, then $X$meets$Y \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Z$.
(85)  If $X \mathrel{{\href{}{\subseteq}}} Y$, then $X$misses$Z \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Y$.
(86)  If $X \mathrel{{\href{}{\subseteq}}} Y$ and $X$misses$Z$, then $X
      \mathrel{{\href{}{\subseteq}}} Y \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} Z$.
(87)  Suppose $Y$misses$Z$. Then $(X \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} Y)\mathop{{\href{xboole_0.html#func2}{\cup}}} Z \mathrel{
      {\href{}{=}}} (X\mathop{{\href{xboole_0.html#func2}{\cup}}} Z) \mathop{
      {\href{xboole_0.html#func4}{\setminus}}} Y$.
(88)  If $X$misses$Y$, then $(X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y)
      \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y \mathrel{{\href{}{=}}}
      X$.
(89)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} Y$misses$X \mathop{{\href
      {xboole_0.html#func4}{\setminus}}} Y$.
(90)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} X \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Y$misses$Y$.
(91)  $(X{\href{xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}
      {\dot-}}} Y){\href{xboole_0.html#func5}{ \mathop{}}{\href
      {xboole_0.html#func5}{\dot-}}} Z \mathrel{{\href{}{=}}} X{\href
      {xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}{\dot-}}} (Y
      {\href{xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}{\dot-
      }}} Z)$.
(92)  $X{\href{xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}
      {\dot-}}} X \mathrel{{\href{}{=}}} {\href{xboole_0.html#func1}
      {\emptyset}}$.
(93)  $X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y \mathrel{{\href{}{=}}} (X
      {\href{xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}{\dot-
      }}} Y)\mathop{{\href{xboole_0.html#func2}{\cup}}} X \mathop{{\href
      {xboole_0.html#func3}{\cap}}} Y$.
(94)  $X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y \mathrel{{\href{}{=}}} (X
      {\href{xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}{\dot-
      }}} Y){\href{xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}
      {\dot-}}} X \mathop{{\href{xboole_0.html#func3}{\cap}}} Y$.
(95)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} Y \mathrel{{\href{}{=}}}
      (X{\href{xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}
      {\dot-}}} Y){\href{xboole_0.html#func5}{ \mathop{}}{\href
      {xboole_0.html#func5}{\dot-}}} (X\mathop{{\href{xboole_0.html#func2}
      {\cup}}} Y)$.
(96)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y \mathrel{{\href{}
      {\subseteq}}} X{\href{xboole_0.html#func5}{ \mathop{}}{\href
      {xboole_0.html#func5}{\dot-}}} Y$.
(97)  Suppose $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y \mathrel{
      {\href{}{\subseteq}}} Z$ and $Y \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} X \mathrel{{\href{}{\subseteq}}} Z$. Then $X{\href
      {xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}{\dot-}}} Y
      \mathrel{{\href{}{\subseteq}}} Z$.
(98)  $X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y \mathrel{{\href{}{=}}} X
      {\href{xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}{\dot-
      }}} (Y \mathop{{\href{xboole_0.html#func4}{\setminus}}} X)$.
(99)  $(X{\href{xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}
      {\dot-}}} Y) \mathop{{\href{xboole_0.html#func4}{\setminus}}} Z \mathrel{
      {\href{}{=}}} (X \mathop{{\href{xboole_0.html#func4}{\setminus}}}
      (Y\mathop{{\href{xboole_0.html#func2}{\cup}}} Z))\mathop{{\href
      {xboole_0.html#func2}{\cup}}} (Y \mathop{{\href{xboole_0.html#func4}
      {\setminus}}} (X\mathop{{\href{xboole_0.html#func2}{\cup}}} Z))$.
(100)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} Y \mathrel{{\href{}
       {=}}} X{\href{xboole_0.html#func5}{ \mathop{}}{\href
       {xboole_0.html#func5}{\dot-}}} X \mathop{{\href{xboole_0.html#func3}
       {\cap}}} Y$.
(101)  $X{\href{xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}
       {\dot-}}} Y \mathrel{{\href{}{=}}} (X\mathop{{\href{xboole_0.html#func2}
       {\cup}}} Y) \mathop{{\href{xboole_0.html#func4}{\setminus}}} X \mathop{
       {\href{xboole_0.html#func3}{\cap}}} Y$.
(102)  $X \mathop{{\href{xboole_0.html#func4}{\setminus}}} (Y{\href
       {xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}{\dot-}}} Z)
       \mathrel{{\href{}{=}}} (X \mathop{{\href{xboole_0.html#func4}
       {\setminus}}} (Y\mathop{{\href{xboole_0.html#func2}{\cup}}} Z))\mathop{
       {\href{xboole_0.html#func2}{\cup}}} (X \mathop{{\href
       {xboole_0.html#func3}{\cap}}} Y) \mathop{{\href{xboole_0.html#func3}
       {\cap}}} Z$.
(103)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} Y$misses$X{\href
       {xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}{\dot-}}}
       Y$.
(104)  $X \mathrel{{\href{}{\subset}}} Y$ or $X \mathrel{{\href{}{=}}} Y$ or $Y
       \mathrel{{\href{}{\subset}}} X$ if and only if $X$ and $Y$ are \hbox
       {$\subseteq$}-comparable.
                             **** 2. Appendix ****
Now we state the propositions:
(105)  Let us consider sets $X$, $Y$. Suppose $X \mathrel{{\href{}{\subset}}}
       Y$. Then $Y \mathop{{\href{xboole_0.html#func4}{\setminus}}} X\mathrel{
       {\href{}{\neq}}} {\href{xboole_0.html#func1}{\emptyset}}$.
(106)  If $X \mathrel{{\href{}{\subseteq}}} A \mathop{{\href
       {xboole_0.html#func4}{\setminus}}} B$, then $X \mathrel{{\href{}
       {\subseteq}}} A$ and $X$misses$B$.
(107)  $X \mathrel{{\href{}{\subseteq}}} A{\href{xboole_0.html#func5}{ \mathop
       {}}{\href{xboole_0.html#func5}{\dot-}}} B$ if and only if $X \mathrel{
       {\href{}{\subseteq}}} A\mathop{{\href{xboole_0.html#func2}{\cup}}} B$
       and $X$misses$A \mathop{{\href{xboole_0.html#func3}{\cap}}} B$.
(108)  If $X \mathrel{{\href{}{\subseteq}}} A$, then $X \mathop{{\href
       {xboole_0.html#func3}{\cap}}} Y \mathrel{{\href{}{\subseteq}}} A$.
(109)  If $X \mathrel{{\href{}{\subseteq}}} A$, then $X \mathop{{\href
       {xboole_0.html#func4}{\setminus}}} Y \mathrel{{\href{}{\subseteq}}} A$.
(110)  If $X \mathrel{{\href{}{\subseteq}}} A$ and $Y \mathrel{{\href{}
       {\subseteq}}} A$, then $X{\href{xboole_0.html#func5}{ \mathop{}}{\href
       {xboole_0.html#func5}{\dot-}}} Y \mathrel{{\href{}{\subseteq}}} A$.
(111)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} Z \mathop{{\href
       {xboole_0.html#func4}{\setminus}}} Y \mathop{{\href{xboole_0.html#func3}
       {\cap}}} Z \mathrel{{\href{}{=}}} (X \mathop{{\href{xboole_0.html#func4}
       {\setminus}}} Y) \mathop{{\href{xboole_0.html#func3}{\cap}}} Z$.
(112)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} Z{\href
       {xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}{\dot-}}} Y
       \mathop{{\href{xboole_0.html#func3}{\cap}}} Z \mathrel{{\href{}{=}}} (X
       {\href{xboole_0.html#func5}{ \mathop{}}{\href{xboole_0.html#func5}{\dot-
       }}} Y) \mathop{{\href{xboole_0.html#func3}{\cap}}} Z$.
(113)  $((X\mathop{{\href{xboole_0.html#func2}{\cup}}} Y)\mathop{{\href
       {xboole_0.html#func2}{\cup}}} Z)\mathop{{\href{xboole_0.html#func2}
       {\cup}}} V \mathrel{{\href{}{=}}} X\mathop{{\href{xboole_0.html#func2}
       {\cup}}} ((Y\mathop{{\href{xboole_0.html#func2}{\cup}}} Z)\mathop{{\href
       {xboole_0.html#func2}{\cup}}} V)$.
(114)  Let us consider sets $A$, $B$, $C$, $D$. Suppose
          i. $A$misses$D$, and
         ii. $B$misses$D$, and
        iii. $C$misses$D$.
       Then $(A\mathop{{\href{xboole_0.html#func2}{\cup}}} B)\mathop{{\href
       {xboole_0.html#func2}{\cup}}} C$misses$D$.
(115)  $A \mathrel{{\href{}{\not\subset}}} {\href{xboole_0.html#func1}
       {\emptyset}}$.
(116)  $X \mathop{{\href{xboole_0.html#func3}{\cap}}} (Y \mathop{{\href
       {xboole_0.html#func3}{\cap}}} Z) \mathrel{{\href{}{=}}} (X \mathop{
       {\href{xboole_0.html#func3}{\cap}}} Y) \mathop{{\href
       {xboole_0.html#func3}{\cap}}} (X \mathop{{\href{xboole_0.html#func3}
       {\cap}}} Z)$.
(117)  Let us consider sets $P$, $G$, $C$. Suppose $C \mathrel{{\href{}
       {\subseteq}}} G$. Then $P \mathop{{\href{xboole_0.html#func4}
       {\setminus}}} C \mathrel{{\href{}{=}}} (P \mathop{{\href
       {xboole_0.html#func4}{\setminus}}} G)\mathop{{\href{xboole_0.html#func2}
       {\cup}}} P \mathop{{\href{xboole_0.html#func3}{\cap}}} (G \mathop{{\href
       {xboole_0.html#func4}{\setminus}}} C)$.
                            Received April 08, 2002
===============================================================================