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;