Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Properties of Subsets

by
Zinaida Trybulec

MML identifier: SUBSET_1
[ Mizar article, MML identifier index ]

```environ

vocabulary BOOLE, SUBSET_1, NEWTON;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
constructors TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
clusters XBOOLE_0;
requirements BOOLE;

begin

reserve E,X,x,y for set;

definition let X be set;
cluster bool X -> non empty;
end;

definition let x;
cluster { x } -> non empty;
let y;
cluster { x, y } -> non empty;
end;

definition let X;
canceled;

mode Element of X means
:: SUBSET_1:def 2
it in X if X is non empty
otherwise it is empty;
end;

definition let X;
mode Subset of X is Element of bool X;
end;

definition let X be non empty set;
cluster non empty Subset of X;
end;

definition let X1,X2 be non empty set;
cluster [: X1,X2 :] -> non empty;
end;

definition let X1,X2,X3 be non empty set;
cluster [: X1,X2,X3 :] -> non empty;
end;

definition let X1,X2,X3,X4 be non empty set;
cluster [: X1,X2,X3,X4 :] -> non empty;
end;

definition let D be non empty set, X be non empty Subset of D;
redefine mode Element of X -> Element of D;
end;

definition let E;
cluster empty Subset of E;
end;

definition let E;
func {} E -> empty Subset of E equals
:: SUBSET_1:def 3
{};
func [#] E -> Subset of E equals
:: SUBSET_1:def 4
E;
end;

canceled 3;

theorem :: SUBSET_1:4
{} is Subset of X;

reserve A,B,C for Subset of E;

canceled 2;

theorem :: SUBSET_1:7
(for x being Element of E holds x in A implies x in B) implies A c= B;

theorem :: SUBSET_1:8
(for x being Element of E holds x in A iff x in B) implies A = B;

canceled;

theorem :: SUBSET_1:10
A <> {} implies ex x being Element of E st x in A;

definition let E,A;
func A` -> Subset of E equals
:: SUBSET_1:def 5
E \ A;
involutiveness;
let B;
redefine func A \/ B -> Subset of E;
func A /\ B -> Subset of E;
func A \ B -> Subset of E;
func A \+\ B -> Subset of E;
end;

canceled 4;

theorem :: SUBSET_1:15
(for x being Element of E holds x in A iff x in B or x in C)
implies A = B \/ C;

theorem :: SUBSET_1:16
(for x being Element of E holds x in A iff x in B & x in C)
implies A = B /\ C;

theorem :: SUBSET_1:17
(for x being Element of E holds x in A iff x in B & not x in C)
implies A = B \ C;

theorem :: SUBSET_1:18
(for x being Element of E holds x in A iff not(x in B iff x in C))
implies A = B \+\ C;

canceled 2;

theorem :: SUBSET_1:21
{} E = ([#] E)`;

theorem :: SUBSET_1:22
[#] E = ({} E)`;

canceled 2;

theorem :: SUBSET_1:25
A \/ A` = [#]E;

theorem :: SUBSET_1:26
A misses A`;

canceled;

theorem :: SUBSET_1:28
A \/ [#]E = [#]E;

theorem :: SUBSET_1:29
(A \/ B)` = A` /\ B`;

theorem :: SUBSET_1:30
(A /\ B)` = A` \/ B`;

theorem :: SUBSET_1:31
A c= B iff B` c= A`;

theorem :: SUBSET_1:32
A \ B = A /\ B`;

theorem :: SUBSET_1:33
(A \ B)` = A` \/ B;

theorem :: SUBSET_1:34
(A \+\ B)` = A /\ B \/ A` /\ B`;

theorem :: SUBSET_1:35
A c= B` implies B c= A`;

theorem :: SUBSET_1:36
A` c= B implies B` c= A;

canceled;

theorem :: SUBSET_1:38
A c= A` iff A = {}E;

theorem :: SUBSET_1:39
A` c= A iff A = [#]E;

theorem :: SUBSET_1:40
X c= A & X c= A` implies X = {};

theorem :: SUBSET_1:41
(A \/ B)` c= A`;

theorem :: SUBSET_1:42
A` c= (A /\ B)`;

theorem :: SUBSET_1:43
A misses B iff A c= B`;

theorem :: SUBSET_1:44
A misses B` iff A c= B;

canceled;

theorem :: SUBSET_1:46
A misses B & A` misses B` implies A = B`;

theorem :: SUBSET_1:47
A c= B & C misses B implies A c= C`;

::
::

theorem :: SUBSET_1:48
(for a being Element of A holds a in B) implies A c= B;

theorem :: SUBSET_1:49
(for x being Element of E holds x in A) implies E = A;

theorem :: SUBSET_1:50
E <> {} implies for B for x being Element of E st not x in B holds x in B`;

theorem :: SUBSET_1:51
for A,B st for x being Element of E holds x in A iff not x in B
holds A = B`;

theorem :: SUBSET_1:52
for A,B st for x being Element of E holds not x in A iff x in B
holds A = B`;

theorem :: SUBSET_1:53
for A,B st for x being Element of E holds not(x in A iff x in B)
holds A = B`;

theorem :: SUBSET_1:54
x in A` implies not x in A;

reserve x1,x2,x3,x4,x5,x6,x7,x8 for Element of X;

theorem :: SUBSET_1:55
X <> {} implies {x1} is Subset of X;

theorem :: SUBSET_1:56
X <> {} implies {x1,x2} is Subset of X;

theorem :: SUBSET_1:57
X <> {} implies {x1,x2,x3} is Subset of X;

theorem :: SUBSET_1:58
X <> {} implies {x1,x2,x3,x4} is Subset of X;

theorem :: SUBSET_1:59
X <> {} implies {x1,x2,x3,x4,x5} is Subset of X;

theorem :: SUBSET_1:60
X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X;

theorem :: SUBSET_1:61
X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X;

theorem :: SUBSET_1:62
X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X;

theorem :: SUBSET_1:63
x in X implies {x} is Subset of X;

scheme Subset_Ex { A()-> set, P[set] } :
ex X being Subset of A() st for x holds x in X iff x in A() & P[x];

scheme Subset_Eq {X() -> set, P[set]}:
for X1,X2 being Subset of X() st
(for y being Element of X() holds y in X1 iff P[y]) &
(for y being Element of X() holds y in X2 iff P[y]) holds
X1 = X2;

definition let X, Y be non empty set;
redefine pred X misses Y;
irreflexivity;
antonym X meets Y;
end;

definition
let S be set; assume