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 $A$ misses $D$, and $B$ misses $D$, and $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