B.9 SUBSET_1

Properties of Subsets by Zinaida Trybulec

reserve E,X,x,y for set;

cluster bool X -> non empty;
cluster { x } -> non empty;
cluster { x, y } -> non empty;

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

mode Subset of X is Element of bool X;

cluster non empty Subset of X;

cluster [: X1,X2 :] -> non empty;

cluster [: X1,X2,X3 :] -> non empty;

cluster [: X1,X2,X3,X4 :] -> non empty;

redefine mode Element of X -> Element of D;

cluster empty Subset of E;

def 3 func {} E -> empty Subset of E equals {};
def 4 func [#] E -> Subset of E equals E;

4 {} is Subset of X;

reserve A,B,C for Subset of E;

7 (for x being Element of E holds x in A implies x in B)
    implies A c= B;
8 (for x being Element of E holds x in A iff x in B) implies A = B;
10 A <> {} implies ex x being Element of E st x in A;

def 5 func A` -> Subset of E equals E \ A;
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;

15 (for x being Element of E holds x in A iff x in B or x in C)
     implies A = B \/ C;
16 (for x being Element of E holds x in A iff x in B & x in C)
     implies A = B /\ C;
17 (for x being Element of E holds x in A iff x in B & not x in C)
     implies A = B \ C;
18 (for x being Element of E holds x in A iff not(x in B iff x in C))
     implies A = B \+\ C;
21 {} E = ([#] E)`;
22 [#] E = ({} E)`;
25 A \/ A` = [#]E;
26 A misses A`;
28 A \/ [#]E = [#]E;
29 (A \/ B)` = A` /\ B`;
30 (A /\ B)` = A` \/ B`;
31 A c= B iff B` c= A`;
32 A \ B = A /\ B`;
33 (A \ B)` = A` \/ B;
34 (A \+\ B)` = A /\ B \/ A` /\ B`;
35 A c= B` implies B c= A`;
36 A` c= B implies B` c= A;
38 A c= A` iff A = {}E;
39 A` c= A iff A = [#]E;
40 X c= A & X c= A` implies X = {};
41 (A \/ B)` c= A`;
42 A` c= (A /\ B)`;
43 A misses B iff A c= B`;
44 A misses B` iff A c= B;
46 A misses B & A` misses B` implies A = B`;
47 A c= B & C misses B implies A c= C`;
48 (for a being Element of A holds a in B) implies A c= B;
49 (for x being Element of E holds x in A) implies E = A;
50 E <> {} implies for A,B holds A = B` iff
    for x being Element of E holds x in A iff not x in B;
51 E <> {} implies for A,B holds A = B` iff
    for x being Element of E holds not x in A iff x in B;
52 E <> {} implies for A,B holds A = B` iff
    for x being Element of E holds not(x in A iff x in B);
53 x in A` implies not x in A;

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

54 X <> {} implies {x1} is Subset of X;
55 X <> {} implies {x1,x2} is Subset of X;
56 X <> {} implies {x1,x2,x3} is Subset of X;
57 X <> {} implies {x1,x2,x3,x4} is Subset of X;
58 X <> {} implies {x1,x2,x3,x4,x5} is Subset of X;
59 X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X;
60 X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X;
61 X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X;
62 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;

redefine pred X misses Y;