The Mizar article:

Properties of Subsets

by
Zinaida Trybulec

Received March 4, 1989

Copyright (c) 1989 Association of Mizar Users

MML identifier: SUBSET_1
[ 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;
 definitions TARSKI, XBOOLE_0;
 theorems XBOOLE_0, TARSKI, ENUMSET1, ZFMISC_1, XBOOLE_1;
 schemes XBOOLE_0;

begin

reserve E,X,x,y for set;

definition let X be set;
 cluster bool X -> non empty;
  coherence by ZFMISC_1:def 1;
end;

definition let x;
 cluster { x } -> non empty;
  coherence by TARSKI:def 1;
  let y;
 cluster { x, y } -> non empty;
  coherence by TARSKI:def 2;
end;

definition let X;
 canceled;

 mode Element of X means
:Def2: it in X if X is non empty
   otherwise it is empty;
 existence by XBOOLE_0:def 1;
 consistency;
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;
 existence
  proof
      X in bool X by ZFMISC_1:def 1;
    then X is Subset of X by Def2;
   hence thesis;
  end;
end;

definition let X1,X2 be non empty set;
  cluster [: X1,X2 :] -> non empty;
 coherence
  proof
   consider x1 being set such that
A1: x1 in X1 by XBOOLE_0:def 1;
   consider x2 being set such that
A2: x2 in X2 by XBOOLE_0:def 1;
     [x1,x2] in [:X1,X2:] by A1,A2,ZFMISC_1:def 2;
   hence thesis;
  end;
end;

definition let X1,X2,X3 be non empty set;
  cluster [: X1,X2,X3 :] -> non empty;
 coherence
  proof
   consider x12 being set such that
A1: x12 in [:X1,X2:] by XBOOLE_0:def 1;
   consider x3 being set such that
A2: x3 in X3 by XBOOLE_0:def 1;
     [x12,x3] in [:[:X1,X2:],X3:] by A1,A2,ZFMISC_1:def 2;
   hence thesis by ZFMISC_1:def 3;
  end;
end;

definition let X1,X2,X3,X4 be non empty set;
  cluster [: X1,X2,X3,X4 :] -> non empty;
 coherence
  proof
   consider x123 being set such that
A1: x123 in [:X1,X2,X3:] by XBOOLE_0:def 1;
   consider x4 being set such that
A2: x4 in X4 by XBOOLE_0:def 1;
     [x123,x4] in [:[:X1,X2,X3:],X4:] by A1,A2,ZFMISC_1:def 2;
   hence thesis by ZFMISC_1:def 4;
  end;
end;

definition let D be non empty set, X be non empty Subset of D;
 redefine mode Element of X -> Element of D;
 coherence
  proof let x be Element of X;
A1:  x in X by Def2;
      X in bool D by Def2;
    then X c= D by ZFMISC_1:def 1;
    then x in D by A1,TARSKI:def 3;
   hence x is Element of D by Def2;
  end;
end;

Lm1:
 for X being Subset of E, x being set st x in X
  holds x in E
proof let X be Subset of E, x be set such that
A1: x in X;
    X in bool E by Def2;
  then X c= E by ZFMISC_1:def 1;
 hence x in E by A1,TARSKI:def 3;
end;

definition let E;
   cluster empty Subset of E;
   existence
     proof
         {} c= E by XBOOLE_1:2;
       then {} in bool E by ZFMISC_1:def 1;
       then {} is Subset of E by Def2;
      hence thesis;
     end;
 end;

definition let E;
  func {} E -> empty Subset of E equals
   {};
   coherence
    proof
        {} c= E by XBOOLE_1:2;
      then {} in bool E by ZFMISC_1:def 1;
     hence thesis by Def2;
    end;
    correctness;
   func [#] E -> Subset of E equals :Def4: E;
    coherence
      proof
         E in bool E by ZFMISC_1:def 1;
       hence E is Subset of E by Def2;
      end;
     correctness;
  end;

canceled 3;

theorem
  {} is Subset of X
proof
    {}X = {};
 hence {} is Subset of X;
end;

 reserve A,B,C for Subset of E;

canceled 2;

theorem
Th7: (for x being Element of E holds x in A implies x in B) implies A c= B
proof
 assume A1: for x being Element of E holds x in A implies x in B;
   let x be set;
    assume A2: x in A;
     then x in E by Lm1;
     then x is Element of E by Def2;
    hence thesis by A1,A2;
end;

theorem Th8:
(for x being Element of E holds x in A iff x in B) implies A = B
proof
  assume for x being Element of E holds x in A iff x in B;
  hence A c= B & B c= A by Th7;
end;

canceled;

theorem
    A <> {} implies ex x being Element of E st x in A
proof
  assume A <> {};
  then consider x being set such that
A1: x in A by XBOOLE_0:def 1;
  x in E by A1,Lm1;
  then x is Element of E by Def2;
  hence thesis by A1;
end;

definition let E,A;
  func A` -> Subset of E equals :Def5: E \ A;
   coherence
    proof
      E \ A c= E by XBOOLE_1:36;
      then E \ A in bool E by ZFMISC_1:def 1;
     hence thesis by Def2;
    end;
   correctness;
   involutiveness
    proof let S,T be Subset of E;
     assume
A1:     S = E \ T;
        T in bool E by Def2;
      then T c= E by ZFMISC_1:def 1;
     hence T = {} \/ E /\ T by XBOOLE_1:28
         .= (E \ E) \/ E /\ T by XBOOLE_1:37
         .= E \ S by A1,XBOOLE_1:52;
    end;
  let B;
  redefine func A \/ B -> Subset of E;
   coherence
    proof
        A in bool E & B in bool E by Def2;
      then A c= E & B c= E by ZFMISC_1:def 1;
      then A \/ B c= E by XBOOLE_1:8;
      then A \/ B in bool E by ZFMISC_1:def 1;
     hence thesis by Def2;
    end;
  func A /\ B -> Subset of E;
   coherence
    proof
A2:    A in bool E by Def2;
A3:    A /\ B c= A by XBOOLE_1:17;
        A c= E by A2,ZFMISC_1:def 1;
      then A /\ B c= E by A3,XBOOLE_1:1;
      then A /\ B in bool E by ZFMISC_1:def 1;
     hence A /\ B is Subset of E by Def2;
    end;
  func A \ B -> Subset of E;
   coherence
    proof
A4:    A in bool E by Def2;
A5:    A \ B c= A by XBOOLE_1:36;
        A c= E by A4,ZFMISC_1:def 1;
      then A \ B c= E by A5,XBOOLE_1:1;
      then A \ B in bool E by ZFMISC_1:def 1;
     hence A \ B is Subset of E by Def2;
    end;
  func A \+\ B -> Subset of E;
   coherence
    proof
A6:    A in bool E & B in bool E by Def2;
     A7: A \ B c= A & B \ A c= B by XBOOLE_1:36;
       A c= E & B c= E by A6,ZFMISC_1:def 1;
     then A \ B c= E & B \ A c= E by A7,XBOOLE_1:1;
     then (A \ B) \/ (B \ A) c= E by XBOOLE_1:8;
      then A \+\ B c= E by XBOOLE_0:def 6;
      then A \+\ B in bool E by ZFMISC_1:def 1;
     hence A \+\ B is Subset of E by Def2;
    end;
 end;

canceled 4;

theorem
  (for x being Element of E holds x in A iff x in B or x in C)
                                           implies A = B \/ C
proof
  assume A1: for x being Element of E holds x in A iff x in B or x in C;
    now
  let x be Element of E;
   assume x in A;
    then x in B or x in C by A1;
   hence x in B \/ C by XBOOLE_0:def 2;
  end;
   hence A c= B \/ C by Th7;
     now
   let x be Element of E;
   assume x in B \/ C;
     then x in B or x in C by XBOOLE_0:def 2;
     hence x in A by A1;
   end;
    hence thesis by Th7;
end;

theorem
  (for x being Element of E holds x in A iff x in B & x in C)
                                           implies A = B /\ C
proof
  assume A1: for x being Element of E holds x in A iff x in B & x in C;
    now
   let x be Element of E;
   assume x in A;
   then x in B & x in C by A1;
   hence x in B /\ C by XBOOLE_0:def 3;
  end;
   hence A c= B /\ C by Th7;
    now
   let x be Element of E;
   assume x in B /\ C;
   then x in B & x in C by XBOOLE_0:def 3;
   hence x in A by A1;
  end;
  hence thesis by Th7;
end;

theorem
  (for x being Element of E holds x in A iff x in B & not x in C)
                                           implies A = B \ C
proof
  assume A1: for x being Element of E holds x in A iff x in B & not x in C;
    now
   let x be Element of E;
   assume x in A;
   then x in B & not x in C by A1;
   hence x in B \ C by XBOOLE_0:def 4;
  end;
   hence A c= B \ C by Th7;
     now
    let x be Element of E;
     assume x in B \ C;
     then x in B & not x in C by XBOOLE_0:def 4;
     hence x in A by A1;
   end;
   hence B \ C c= A by Th7;
end;

theorem
  (for x being Element of E holds x in A iff not(x in B iff x in C))
                                     implies A = B \+\ C
proof
  assume A1: for x being Element of E holds x in A iff not(x in B iff x in C);
    now
   let x be Element of E;
   assume x in A;
   then x in B & not x in C or x in C & not x in B by A1;
   then x in B \ C or x in C \ B by XBOOLE_0:def 4;
   then x in (B \ C) \/ (C \ B) by XBOOLE_0:def 2;
   hence x in B \+\ C by XBOOLE_0:def 6;
  end;
   hence A c= B \+\ C by Th7;
    now
   let x be Element of E;
   assume x in B \+\ C;
   then x in (B \ C) \/ (C \ B) by XBOOLE_0:def 6;
   then x in B \ C or x in C \ B by XBOOLE_0:def 2;
   then x in B & not x in C or x in C & not x in B by XBOOLE_0:def 4;
   hence x in A by A1;
  end;
   hence thesis by Th7;
end;

canceled 2;

theorem
 Th21: {} E = ([#] E)`
proof
 thus ([#]E)` = E \ [#]E by Def5
           .= E \ E by Def4
           .= {}E by XBOOLE_1:37;
end;

theorem
 Th22: [#] E = ({} E)`
proof
 thus [#]E = E \ {} by Def4
        .= ({}E)` by Def5;
end;

canceled 2;

theorem
Th25: A \/ A` = [#]E
proof
   A in bool E by Def2;
then A1: A c= E by ZFMISC_1:def 1;
  thus A \/ A` = A \/ (E \ A) by Def5
             .= E by A1,XBOOLE_1:45
             .= [#] E by Def4;
end;

theorem Th26:
  A misses A`
proof
A1:A misses (E \ A) by XBOOLE_1:79;
    A /\ A` = A /\ (E \ A) by Def5
             .= {} by A1,XBOOLE_0:def 7;
  hence thesis by XBOOLE_0:def 7;
end;

canceled;

theorem
    A \/ [#]E = [#]E
 proof
   A in bool E by Def2;
then A1: A c= E by ZFMISC_1:def 1;
   thus A \/ [#]E = A \/ E by Def4
              .= E by A1,XBOOLE_1:12
              .= [#]E by Def4;
 end;

theorem
    (A \/ B)` = A` /\ B`
proof
  thus (A \/ B)` = E \ (A \/ B) by Def5
                .= (E \ A) /\ (E \ B) by XBOOLE_1:53
                .= A` /\ (E \ B) by Def5
                .= A` /\ B` by Def5;
end;

theorem
    (A /\ B)` = A` \/ B`
proof
  thus (A /\ B)` = E \ (A /\ B) by Def5
                .= (E \ A) \/ (E \ B) by XBOOLE_1:54
                .= A` \/ (E \ B) by Def5
                .= A` \/ B` by Def5;
end;

theorem
Th31: A c= B iff B` c= A`
proof
    E \ A = A` & E \ B = B` by Def5;
  hence A c= B implies B` c= A` by XBOOLE_1:34;
    A1: E \ A` = A`` by Def5 .= A;
         E \ B` = B`` by Def5 .= B;
    hence thesis by A1,XBOOLE_1:34;
end;

theorem
   A \ B = A /\ B`
proof
     A in bool E by Def2;
then A1: A c= E by ZFMISC_1:def 1;
  thus A /\ B` = A /\ (E \ B) by Def5
             .= (A /\ E) \ B by XBOOLE_1:49
             .= A \ B by A1,XBOOLE_1:28;
end;

theorem
    (A \ B)` = A` \/ B
proof
     A in bool E & B in bool E by Def2;
then A1: A c= E & B c= E by ZFMISC_1:def 1;
  thus (A \ B)` = E \ (A \ B) by Def5
               .= (E \ A) \/ E /\ B by XBOOLE_1:52
               .= A` \/ E /\ B by Def5
               .= A` \/ B by A1,XBOOLE_1:28;
end;

theorem
    (A \+\ B)` = A /\ B \/ A` /\ B`
proof
     A in bool E by Def2;
then A1: A c= E by ZFMISC_1:def 1;
  thus (A \+\ B)` = E \ (A \+\ B) by Def5
               .= E \ (A \/ B) \/ E /\ A /\ B by XBOOLE_1:102
               .= A /\ B \/ (E \ (A \/ B)) by A1,XBOOLE_1:28
               .= A /\ B \/ (E \ A) /\ (E \ B) by XBOOLE_1:53
               .= A /\ B \/ A` /\ (E \ B) by Def5
               .= A /\ B \/ (A`) /\ (B`) by Def5;
end;

theorem
   A c= B` implies B c= A`
proof
  assume A c= B`;
  then B``c= A` by Th31;
  hence thesis;
end;

theorem
   A` c= B implies B` c= A
proof
  assume A` c= B;
  then B` c= A`` by Th31;
  hence thesis;
end;

canceled;

theorem
   A c= A` iff A = {}E
  proof
   thus A c= A` implies A = {}E
    proof
     assume A c= A`;
     then A c= E \ A by Def5;
     hence thesis by XBOOLE_1:38;
    end;
A1: A in bool E by Def2;
   assume A = {}E;
    then A` = [#]E by Th22 .= E by Def4;
   hence A c= A` by A1,ZFMISC_1:def 1;
  end;

theorem
   A` c= A iff A = [#]E
  proof
   thus A` c= A implies A = [#]E
    proof
     assume A` c= A;
     hence A = A \/ A` by XBOOLE_1:12
            .= [#]E by Th25;
    end;
   assume A = [#]E;
    then A` = {}E by Th21 .= {};
   hence A` c= A by XBOOLE_1:2;
  end;

theorem
   X c= A & X c= A` implies X = {}
  proof
     A misses A` by Th26;
   hence thesis by XBOOLE_1:67;
  end;

theorem
   (A \/ B)` c= A`
  proof
     A c= A \/ B by XBOOLE_1:7;
   hence thesis by Th31;
  end;

theorem
   A` c= (A /\ B)`
  proof
     A /\ B c= A by XBOOLE_1:17;
   hence thesis by Th31;
  end;

theorem
Th43: A misses B iff A c= B`
proof
  thus A misses B implies A c= B`
    proof
      assume
A1:     A misses B;
      let x;
      assume A2: x in A;
      then A3: x in E by Lm1;
        not x in B by A1,A2,XBOOLE_0:3;
      then x in E \ B by A3,XBOOLE_0:def 4;
      hence x in B` by Def5;
    end;
    assume A4: A c= B`;
    assume A meets B;
    then consider x such that
A5: x in A & x in B by XBOOLE_0:3;
      A c= E \ B by A4,Def5;
    then x in E \ B by A5,TARSKI:def 3;
    hence thesis by A5,XBOOLE_0:def 4;
end;

theorem
   A misses B` iff A c= B
  proof
     B``= B;
   hence thesis by Th43;
  end;

canceled;

theorem
   A misses B & A` misses B` implies A = B`
proof
A1: A in bool E by Def2;
  assume that A2: A misses B and
              A3: A` misses B`;
    thus A c= B`
     proof
      let x;
      assume A4: x in A;
        A c= E by A1,ZFMISC_1:def 1;
then A5:   x in E by A4,TARSKI:def 3;
        not x in B by A2,A4,XBOOLE_0:3;
      then x in E \ B by A5,XBOOLE_0:def 4;
      hence thesis by Def5;
     end;
     let x;
     assume x in B`;
     then x in E \ B by Def5;
     then A6: x in E & not x in B by XBOOLE_0:def 4;
       x in A` implies not x in B` by A3,XBOOLE_0:3;
     then x in E \ A implies not x in E \ B by Def5;
     hence thesis by A6,XBOOLE_0:def 4;
end;

theorem
   A c= B & C misses B implies A c= C`
  proof
   assume A c= B & C misses B;
   then A misses C by XBOOLE_1:63;
   hence thesis by Th43;
  end;

 ::
 ::                 ADDITIONAL THEOREMS
 ::

theorem
  (for a being Element of A holds a in B) implies A c= B
proof
  assume A1: for a being Element of A holds a in B;
   let a be set;
   assume
   a in A;
   then a is Element of A by Def2;
  hence thesis by A1;
end;

theorem
  (for x being Element of E holds x in A) implies E = A
proof
  assume A1: for x being Element of E holds x in A;
  thus E c= A
   proof
    let a be set;
    assume
    a in E;
    then a is Element of E by Def2;
    hence thesis by A1;
   end;
     A in bool E by Def2;
  hence A c= E by ZFMISC_1:def 1;
end;

theorem
  E <> {} implies for B for x being Element of E st not x in B holds x in B`
proof
  assume
A1: E <> {};
   let B be Subset of E;
     let x be Element of E;
     assume
A2:    not x in B;
       x in E by A1,Def2;
     then x in E \ B by A2,XBOOLE_0:def 4;
     hence x in B` by Def5;
end;

theorem Th51:
 for A,B st for x being Element of E holds x in A iff not x in B
  holds A = B`
proof
   let A,B be Subset of E;
   assume A1: for x being Element of E holds x in A iff not x in B;
    thus A c= B`
    proof
     let x be set;
     assume A2: x in A;
       A in bool E by Def2;
     then A c= E by ZFMISC_1:def 1;
     then x in E by A2,TARSKI:def 3;
     then x is Element of E by Def2;
     then x in E & not x in B by A1,A2,Lm1;
     then x in E \ B by XBOOLE_0:def 4;
     hence thesis by Def5;
    end;
    let x be set;
A3: B` in bool E by Def2;
    assume A4: x in B`;
      B` c= E by A3,ZFMISC_1:def 1;
    then x in E by A4,TARSKI:def 3;
    then reconsider x as Element of E by Def2;
      x in E \ B by A4,Def5;
    then not x in B by XBOOLE_0:def 4;
    hence thesis by A1;
end;

theorem
   for A,B st for x being Element of E holds not x in A iff x in B
  holds A = B`
 proof
  let A,B;
  assume for x being Element of E holds not x in A iff x in B;
   then for x being Element of E holds x in A iff not x in B;
  hence A = B` by Th51;
 end;

theorem
   for A,B st for x being Element of E holds not(x in A iff x in B)
  holds A = B`
 proof let A,B;
  assume for x being Element of E holds not(x in A iff x in B);
   then for x being Element of E holds x in A iff not x in B;
  hence A = B` by Th51;
 end;

theorem
    x in A` implies not x in A
proof
  assume x in A`;
  then x in E \ A by Def5;
  hence thesis by XBOOLE_0:def 4;
end;

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

theorem
    X <> {} implies {x1} is Subset of X
proof assume
     X <> {};
then A1: x1 in X by Def2;
    {x1} c= X
  proof
   let x;
   assume x in {x1};
   hence x in X by A1,TARSKI:def 1;
  end;
  then {x1} in bool X by ZFMISC_1:def 1;
 hence {x1} is Subset of X by Def2;
end;

theorem
    X <> {} implies {x1,x2} is Subset of X
proof assume X <> {};
then A1: x1 in X & x2 in X by Def2;
   {x1,x2} c= X
 proof
  let x;
  assume x in {x1,x2};
  hence x in X by A1,TARSKI:def 2;
 end;
  then {x1,x2} in bool X by ZFMISC_1:def 1;
 hence {x1,x2} is Subset of X by Def2;
end;

theorem
    X <> {} implies {x1,x2,x3} is Subset of X
proof assume X <> {};
then A1: x1 in X & x2 in X & x3 in X by Def2;
   {x1,x2,x3} c= X
 proof
   let x;
   assume x in {x1,x2,x3};
   hence x in X by A1,ENUMSET1:def 1;
 end;
  then {x1,x2,x3} in bool X by ZFMISC_1:def 1;
 hence {x1,x2,x3} is Subset of X by Def2;
end;

theorem
    X <> {} implies {x1,x2,x3,x4} is Subset of X
proof assume X <> {};
then A1: x1 in X & x2 in X & x3 in X & x4 in X by Def2;
   {x1,x2,x3,x4} c= X
 proof
  let x;
  assume x in {x1,x2,x3,x4};
  hence x in X by A1,ENUMSET1:18;
 end;
  then {x1,x2,x3,x4} in bool X by ZFMISC_1:def 1;
 hence {x1,x2,x3,x4} is Subset of X by Def2;
end;

theorem
    X <> {} implies {x1,x2,x3,x4,x5} is Subset of X
proof assume
A1: X <> {};
   {x1,x2,x3,x4,x5} c= X
 proof
  let x;
  assume
A2:  x in {x1,x2,x3,x4,x5};
     x in { x1,x2,x3,x4,x5 } implies x=x1 or x=x2 or x=x3 or x=x4 or x=x5
                                by ENUMSET1:23;
  hence x in X by A1,A2,Def2;
 end;
  then {x1,x2,x3,x4,x5} in bool X by ZFMISC_1:def 1;
 hence {x1,x2,x3,x4,x5} is Subset of X by Def2;
end;

theorem
    X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X
proof assume
A1: X <> {};
   {x1,x2,x3,x4,x5,x6} c= X
 proof
  let x;
  assume A2: x in {x1,x2,x3,x4,x5,x6};
     x in { x1,x2,x3,x4,x5,x6} implies
     x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 by ENUMSET1:28;
  hence x in X by A1,A2,Def2;
 end;
  then {x1,x2,x3,x4,x5,x6} in bool X by ZFMISC_1:def 1;
 hence {x1,x2,x3,x4,x5,x6} is Subset of X by Def2;
end;

theorem
    X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X
proof assume
A1: X <> {};
   {x1,x2,x3,x4,x5,x6,x7} c= X
 proof
  let x;
  assume A2: x in {x1,x2,x3,x4,x5,x6,x7};
     x in { x1,x2,x3,x4,x5,x6,x7} implies
     x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 by ENUMSET1:33;
  hence x in X by A1,A2,Def2;
 end;
  then {x1,x2,x3,x4,x5,x6,x7} in bool X by ZFMISC_1:def 1;
 hence {x1,x2,x3,x4,x5,x6,x7} is Subset of X by Def2;
end;

theorem
    X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X
proof assume
A1: X <> {};
   {x1,x2,x3,x4,x5,x6,x7,x8} c= X
 proof
  let x;
  assume A2: x in {x1,x2,x3,x4,x5,x6,x7,x8};
     x in { x1,x2,x3,x4,x5,x6,x7,x8} implies
     x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8
                                          by ENUMSET1:38;
  hence x in X by A1,A2,Def2;
 end;
  then {x1,x2,x3,x4,x5,x6,x7,x8} in bool X by ZFMISC_1:def 1;
 hence {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X by Def2;
end;

theorem
    x in X implies {x} is Subset of X
proof assume x in X;
  then {x} c= X by ZFMISC_1:37;
  then {x} in bool X by ZFMISC_1:def 1;
 hence thesis by Def2;
end;

 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]
    proof
     defpred X[set] means P[$1];
     consider X being set such that
A1:   for x holds
        x in X iff x in A() & X[x] from Separation;
        X c= A()
       proof
        let x;
        thus thesis by A1;
       end;
      then X in bool A() by ZFMISC_1:def 1;
      then reconsider X as Subset of A() by Def2;
     take X;
     thus thesis by A1;
    end;

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
proof
 let X1,X2 be Subset of X() such that
A1:for y being Element of X() holds y in X1 iff P[y] and
A2:for y being Element of X() holds y in X2 iff P[y];
    for x being Element of X() holds x in X1 iff x in X2
  proof
    let x be Element of X();
    hereby assume x in X1;
      then P[x] by A1;
      hence x in X2 by A2;
    end;
    assume x in X2;
    then P[x] by A2;
    hence thesis by A1;
  end;
  hence thesis by Th8;
end;

definition let X, Y be non empty set;
 redefine pred X misses Y;
 irreflexivity
  proof
    let A be non empty set;
    consider x being set such that A1: x in A by XBOOLE_0:def 1;
    thus thesis by A1,XBOOLE_0:3;
  end;
 antonym X meets Y;
end;

definition
   let S be set; assume
A1: contradiction;
 func choose S -> Element of S means
    not contradiction;
 correctness by A1;
end;
      


Back to top