Miz-B-7

B.7 SUBSET_1

SUBSET_1.ABS (Digest)
Properties of Subsets, by Zinaida Trybulec.

reserve E,X for set;
reserve x,y for Any;

cluster empty Subset of E;

def 1 func E -> empty Subset of E means it = ;
def 2 func E ->manes it = E;

4 is Subset of X;

reserve A,B,C for Subset of E;

7 (for x being Element of E holds x C A implies x CB) implies A c= B;
8 (for x being Element of E holds x C A iff x C B) implies A = B;


def 3  func A -> Subset of E means it = E  A;

       func A U 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 C A iff x C B or x C C)

     implies A = B U C; 

16 (for x being Element of E holds x C A iff x C B & x C C)

     implies A = B  C;

17 (for x being Element of E holds x C A iff x C B & not x C C)

     implies A = B  C;

18 (for x being Element of E holds x C A iff not(x C B iff x CC))

     implies A = B  C;

20  E = E;

21  E = ( E) ;

22  E = ( E) ;

23 A = E  A;

24 A = A;

25 A U A = E & A U A =  E;

26 A  A= E & A  A = E;

28 A U E = E & E U A = E;

29 (A U B) = A  B

30 (A  B) = A U B;

31 A c= B iff B c= A;

32 A  B = A  B ;

33 (A  B) = A U B;

34 (A  B) = A  B U 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 U B) c= A & (A U B) c= B;

42 A c= (A  B) & B c= (A  B);

43 A misses B iff A c= B;

44 A misses B iff A c= B;

45 A misses A;

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 C B) implies A c= B;

49 (for x being Element of E holds x C A) implies E = A;

50 E < >  implies for A,B holds A = B iff

  for x being Element of E holds x C A iff not x C B;

51 E < >  implies for A,B holds A = B iff

     for x being Element of E holds not x C A iff x C B;

52 E < >  implies for A,B holds A = B iff

     for x being Element of E holds not(x C A iff x C B);

53 x C A implies not x C 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;

reserve x1,x2,x3,x4,x5,x6,x7,x8 for Any;

62 x1 C X implies {x1} is Subset of X;

scheme Subset_Ex { A( )-> set,P[Any] } :

  ex X being Subset of A( ) st for x holds x C X iff x C A( ) & P[x];