xregular.miz



    begin

    reserve x,y,X1,X2,X3,X4,X5,X6,Y,Y1,Y2,Y3,Y4,Y5,Z,Z1,Z2,Z3,Z4,Z5 for set;

    reserve X for non empty set;

    theorem :: XREGULAR:1

    

     Th1: ex Y st Y in X & Y misses X

    proof

      consider x be object such that

       A1: x in X by XBOOLE_0:def 1;

      consider Y such that

       A2: Y in X and

       A3: not ex x be object st x in X & x in Y by A1, TARSKI: 3;

      take Y;

       not ex x be object st x in X & x in Y by A3;

      hence thesis by A2, XBOOLE_0: 3;

    end;

    theorem :: XREGULAR:2

    ex Y st Y in X & for Y1 st Y1 in Y holds Y1 misses X

    proof

      defpred P[ set] means $1 meets X;

      consider Z such that

       A1: for Y holds Y in Z iff Y in ( union X) & P[Y] from XFAMILY:sch 1;

      consider Y such that

       A2: Y in (X \/ Z) and

       A3: Y misses (X \/ Z) by Th1;

      assume

       A4: not thesis;

      now

        assume

         A5: Y in X;

        then

        consider Y1 such that

         A6: Y1 in Y and

         A7: not Y1 misses X by A4;

        Y1 in ( union X) by A5, A6, TARSKI:def 4;

        then Y1 in Z by A1, A7;

        then Y1 in (X \/ Z) by XBOOLE_0:def 3;

        hence contradiction by A3, A6, XBOOLE_0: 3;

      end;

      then Y in Z by A2, XBOOLE_0:def 3;

      then Y meets X by A1;

      hence contradiction by A3, XBOOLE_1: 70;

    end;

    theorem :: XREGULAR:3

    ex Y st Y in X & for Y1, Y2 st Y1 in Y2 & Y2 in Y holds Y1 misses X

    proof

      defpred P[ set] means ex Y1 st Y1 in $1 & Y1 meets X;

      consider Z1 such that

       A1: for Y holds Y in Z1 iff Y in ( union X) & P[Y] from XFAMILY:sch 1;

      defpred Q[ set] means $1 meets X;

      consider Z2 such that

       A2: for Y holds Y in Z2 iff Y in ( union ( union X)) & Q[Y] from XFAMILY:sch 1;

      consider Y such that

       A3: Y in ((X \/ Z1) \/ Z2) and

       A4: Y misses ((X \/ Z1) \/ Z2) by Th1;

       A5:

      now

        assume

         A6: Y in Z1;

        then

        consider Y1 such that

         A7: Y1 in Y and

         A8: Y1 meets X by A1;

        Y in ( union X) by A1, A6;

        then Y1 in ( union ( union X)) by A7, TARSKI:def 4;

        then Y1 in Z2 by A2, A8;

        then Y1 in ((X \/ Z1) \/ Z2) by XBOOLE_0:def 3;

        hence contradiction by A4, A7, XBOOLE_0: 3;

      end;

      assume

       A9: not thesis;

       A10:

      now

        assume

         A11: Y in X;

        then

        consider Y1, Y2 such that

         A12: Y1 in Y2 and

         A13: Y2 in Y and

         A14: not Y1 misses X by A9;

        Y2 in ( union X) by A11, A13, TARSKI:def 4;

        then Y2 in Z1 by A1, A12, A14;

        then Y2 in (X \/ Z1) by XBOOLE_0:def 3;

        then Y2 in ((X \/ Z1) \/ Z2) by XBOOLE_0:def 3;

        hence contradiction by A4, A13, XBOOLE_0: 3;

      end;

      Y in (X \/ (Z1 \/ Z2)) by A3, XBOOLE_1: 4;

      then Y in (Z1 \/ Z2) by A10, XBOOLE_0:def 3;

      then Y in Z2 by A5, XBOOLE_0:def 3;

      then Y meets X by A2;

      then Y meets (X \/ Z1) by XBOOLE_1: 70;

      hence contradiction by A4, XBOOLE_1: 70;

    end;

    theorem :: XREGULAR:4

    ex Y st Y in X & for Y1, Y2, Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in Y holds Y1 misses X

    proof

      defpred P[ set] means ex Y1, Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X;

      consider Z1 such that

       A1: for Y holds Y in Z1 iff Y in ( union X) & P[Y] from XFAMILY:sch 1;

      defpred R[ set] means $1 meets X;

      defpred Q[ set] means ex Y1 st Y1 in $1 & Y1 meets X;

      consider Z2 such that

       A2: for Y holds Y in Z2 iff Y in ( union ( union X)) & Q[Y] from XFAMILY:sch 1;

      consider Z3 such that

       A3: for Y holds Y in Z3 iff Y in ( union ( union ( union X))) & R[Y] from XFAMILY:sch 1;

      consider Y such that

       A4: Y in (((X \/ Z1) \/ Z2) \/ Z3) and

       A5: Y misses (((X \/ Z1) \/ Z2) \/ Z3) by Th1;

       A6:

      now

        assume

         A7: Y in Z2;

        then

        consider Y1 such that

         A8: Y1 in Y and

         A9: Y1 meets X by A2;

        Y in ( union ( union X)) by A2, A7;

        then Y1 in ( union ( union ( union X))) by A8, TARSKI:def 4;

        then Y1 in Z3 by A3, A9;

        then Y1 in (((X \/ Z1) \/ Z2) \/ Z3) by XBOOLE_0:def 3;

        hence contradiction by A5, A8, XBOOLE_0: 3;

      end;

       A10:

      now

        assume

         A11: Y in Z1;

        then

        consider Y1, Y2 such that

         A12: Y1 in Y2 and

         A13: Y2 in Y and

         A14: Y1 meets X by A1;

        Y in ( union X) by A1, A11;

        then Y2 in ( union ( union X)) by A13, TARSKI:def 4;

        then Y2 in Z2 by A2, A12, A14;

        then Y2 in ((X \/ Z1) \/ Z2) by XBOOLE_0:def 3;

        then Y meets ((X \/ Z1) \/ Z2) by A13, XBOOLE_0: 3;

        hence contradiction by A5, XBOOLE_1: 70;

      end;

      set V = (((X \/ Z1) \/ Z2) \/ Z3);

      

       A15: V = ((X \/ (Z1 \/ Z2)) \/ Z3) by XBOOLE_1: 4

      .= (X \/ ((Z1 \/ Z2) \/ Z3)) by XBOOLE_1: 4;

      assume

       A16: not thesis;

      now

        assume

         A17: Y in X;

        then

        consider Y1, Y2, Y3 such that

         A18: Y1 in Y2 & Y2 in Y3 and

         A19: Y3 in Y and

         A20: not Y1 misses X by A16;

        Y3 in ( union X) by A17, A19, TARSKI:def 4;

        then Y3 in Z1 by A1, A18, A20;

        then Y3 in (X \/ Z1) by XBOOLE_0:def 3;

        then Y3 in ((X \/ Z1) \/ Z2) by XBOOLE_0:def 3;

        then Y3 in (((X \/ Z1) \/ Z2) \/ Z3) by XBOOLE_0:def 3;

        hence contradiction by A5, A19, XBOOLE_0: 3;

      end;

      then Y in ((Z1 \/ Z2) \/ Z3) by A15, A4, XBOOLE_0:def 3;

      then Y in (Z1 \/ (Z2 \/ Z3)) by XBOOLE_1: 4;

      then Y in (Z2 \/ Z3) by A10, XBOOLE_0:def 3;

      then Y in Z3 by A6, XBOOLE_0:def 3;

      then Y meets X by A3;

      hence contradiction by A15, A5, XBOOLE_1: 70;

    end;

    theorem :: XREGULAR:5

    ex Y st Y in X & for Y1, Y2, Y3, Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y holds Y1 misses X

    proof

      defpred P[ set] means ex Y1, Y2, Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X;

      consider Z1 such that

       A1: for Y holds Y in Z1 iff Y in ( union X) & P[Y] from XFAMILY:sch 1;

      defpred S[ set] means $1 meets X;

      defpred R[ set] means ex Y1 st Y1 in $1 & Y1 meets X;

      defpred Q[ set] means ex Y1, Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X;

      consider Z2 such that

       A2: for Y holds Y in Z2 iff Y in ( union ( union X)) & Q[Y] from XFAMILY:sch 1;

      consider Z4 such that

       A3: for Y holds Y in Z4 iff Y in ( union ( union ( union ( union X)))) & S[Y] from XFAMILY:sch 1;

      consider Z3 such that

       A4: for Y holds Y in Z3 iff Y in ( union ( union ( union X))) & R[Y] from XFAMILY:sch 1;

      consider Y such that

       A5: Y in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) and

       A6: Y misses ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) by Th1;

       A7:

      now

        assume

         A8: Y in Z3;

        then

        consider Y1 such that

         A9: Y1 in Y and

         A10: Y1 meets X by A4;

        Y in ( union ( union ( union X))) by A4, A8;

        then Y1 in ( union ( union ( union ( union X)))) by A9, TARSKI:def 4;

        then Y1 in Z4 by A3, A10;

        then Y1 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) by XBOOLE_0:def 3;

        hence contradiction by A6, A9, XBOOLE_0: 3;

      end;

       A11:

      now

        assume

         A12: Y in Z1;

        then

        consider Y1, Y2, Y3 such that

         A13: Y1 in Y2 & Y2 in Y3 and

         A14: Y3 in Y and

         A15: Y1 meets X by A1;

        Y in ( union X) by A1, A12;

        then Y3 in ( union ( union X)) by A14, TARSKI:def 4;

        then Y3 in Z2 by A2, A13, A15;

        then Y3 in ((X \/ Z1) \/ Z2) by XBOOLE_0:def 3;

        then Y meets ((X \/ Z1) \/ Z2) by A14, XBOOLE_0: 3;

        then Y meets (((X \/ Z1) \/ Z2) \/ Z3) by XBOOLE_1: 70;

        hence contradiction by A6, XBOOLE_1: 70;

      end;

      

       A16: ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) = (((X \/ (Z1 \/ Z2)) \/ Z3) \/ Z4) by XBOOLE_1: 4

      .= ((X \/ ((Z1 \/ Z2) \/ Z3)) \/ Z4) by XBOOLE_1: 4

      .= (X \/ (((Z1 \/ Z2) \/ Z3) \/ Z4)) by XBOOLE_1: 4;

       A17:

      now

        assume

         A18: Y in Z2;

        then

        consider Y1, Y2 such that

         A19: Y1 in Y2 and

         A20: Y2 in Y and

         A21: Y1 meets X by A2;

        Y in ( union ( union X)) by A2, A18;

        then Y2 in ( union ( union ( union X))) by A20, TARSKI:def 4;

        then Y2 in Z3 by A4, A19, A21;

        then Y2 in (((X \/ Z1) \/ Z2) \/ Z3) by XBOOLE_0:def 3;

        then Y meets (((X \/ Z1) \/ Z2) \/ Z3) by A20, XBOOLE_0: 3;

        hence contradiction by A6, XBOOLE_1: 70;

      end;

      assume

       A22: not thesis;

      now

        assume

         A23: Y in X;

        then

        consider Y1, Y2, Y3, Y4 such that

         A24: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 and

         A25: Y4 in Y and

         A26: not Y1 misses X by A22;

        Y4 in ( union X) by A23, A25, TARSKI:def 4;

        then Y4 in Z1 by A1, A24, A26;

        then Y4 in (X \/ Z1) by XBOOLE_0:def 3;

        then Y4 in ((X \/ Z1) \/ Z2) by XBOOLE_0:def 3;

        then Y4 in (((X \/ Z1) \/ Z2) \/ Z3) by XBOOLE_0:def 3;

        then Y4 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) by XBOOLE_0:def 3;

        hence contradiction by A6, A25, XBOOLE_0: 3;

      end;

      then Y in (((Z1 \/ Z2) \/ Z3) \/ Z4) by A16, A5, XBOOLE_0:def 3;

      then Y in ((Z1 \/ (Z2 \/ Z3)) \/ Z4) by XBOOLE_1: 4;

      then Y in (Z1 \/ ((Z2 \/ Z3) \/ Z4)) by XBOOLE_1: 4;

      then Y in ((Z2 \/ Z3) \/ Z4) by A11, XBOOLE_0:def 3;

      then Y in (Z2 \/ (Z3 \/ Z4)) by XBOOLE_1: 4;

      then Y in (Z3 \/ Z4) by A17, XBOOLE_0:def 3;

      then Y in Z4 by A7, XBOOLE_0:def 3;

      then Y meets X by A3;

      hence contradiction by A16, A6, XBOOLE_1: 70;

    end;

    theorem :: XREGULAR:6

    ex Y st Y in X & for Y1, Y2, Y3, Y4, Y5 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y holds Y1 misses X

    proof

      defpred P[ set] means ex Y1, Y2, Y3, Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in $1 & Y1 meets X;

      consider Z1 such that

       A1: for Y holds Y in Z1 iff Y in ( union X) & P[Y] from XFAMILY:sch 1;

      defpred T[ set] means $1 meets X;

      defpred S[ set] means ex Y1 st Y1 in $1 & Y1 meets X;

      defpred R[ set] means ex Y1, Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X;

      defpred Q[ set] means ex Y1, Y2, Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X;

      consider Z2 such that

       A2: for Y holds Y in Z2 iff Y in ( union ( union X)) & Q[Y] from XFAMILY:sch 1;

      consider Z5 such that

       A3: for Y holds Y in Z5 iff Y in ( union ( union ( union ( union ( union X))))) & T[Y] from XFAMILY:sch 1;

      consider Z3 such that

       A4: for Y holds Y in Z3 iff Y in ( union ( union ( union X))) & R[Y] from XFAMILY:sch 1;

      consider Z4 such that

       A5: for Y holds Y in Z4 iff Y in ( union ( union ( union ( union X)))) & S[Y] from XFAMILY:sch 1;

      set V = (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5);

      consider Y such that

       A6: Y in V and

       A7: Y misses V by Th1;

      

       A8: V = ((((X \/ (Z1 \/ Z2)) \/ Z3) \/ Z4) \/ Z5) by XBOOLE_1: 4

      .= (((X \/ ((Z1 \/ Z2) \/ Z3)) \/ Z4) \/ Z5) by XBOOLE_1: 4

      .= ((X \/ (((Z1 \/ Z2) \/ Z3) \/ Z4)) \/ Z5) by XBOOLE_1: 4

      .= (X \/ ((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5)) by XBOOLE_1: 4;

       A9:

      now

        assume

         A10: Y in Z1;

        then

        consider Y1, Y2, Y3, Y4 such that

         A11: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 and

         A12: Y4 in Y and

         A13: Y1 meets X by A1;

        Y in ( union X) by A1, A10;

        then Y4 in ( union ( union X)) by A12, TARSKI:def 4;

        then Y4 in Z2 by A2, A11, A13;

        then Y4 in ((X \/ Z1) \/ Z2) by XBOOLE_0:def 3;

        then Y meets ((X \/ Z1) \/ Z2) by A12, XBOOLE_0: 3;

        then Y meets (((X \/ Z1) \/ Z2) \/ Z3) by XBOOLE_1: 70;

        then Y meets ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) by XBOOLE_1: 70;

        hence contradiction by A7, XBOOLE_1: 70;

      end;

       A14:

      now

        assume

         A15: Y in Z2;

        then

        consider Y1, Y2, Y3 such that

         A16: Y1 in Y2 & Y2 in Y3 and

         A17: Y3 in Y and

         A18: Y1 meets X by A2;

        Y in ( union ( union X)) by A2, A15;

        then Y3 in ( union ( union ( union X))) by A17, TARSKI:def 4;

        then Y3 in Z3 by A4, A16, A18;

        then Y3 in (((X \/ Z1) \/ Z2) \/ Z3) by XBOOLE_0:def 3;

        then Y3 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) by XBOOLE_0:def 3;

        then Y3 in V by XBOOLE_0:def 3;

        hence contradiction by A7, A17, XBOOLE_0: 3;

      end;

       A19:

      now

        assume

         A20: Y in Z3;

        then

        consider Y1, Y2 such that

         A21: Y1 in Y2 and

         A22: Y2 in Y and

         A23: Y1 meets X by A4;

        Y in ( union ( union ( union X))) by A4, A20;

        then Y2 in ( union ( union ( union ( union X)))) by A22, TARSKI:def 4;

        then Y2 in Z4 by A5, A21, A23;

        then Y2 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) by XBOOLE_0:def 3;

        then Y2 in V by XBOOLE_0:def 3;

        hence contradiction by A7, A22, XBOOLE_0: 3;

      end;

       A24:

      now

        assume

         A25: Y in Z4;

        then

        consider Y1 such that

         A26: Y1 in Y and

         A27: Y1 meets X by A5;

        Y in ( union ( union ( union ( union X)))) by A5, A25;

        then Y1 in ( union ( union ( union ( union ( union X))))) by A26, TARSKI:def 4;

        then Y1 in Z5 by A3, A27;

        then Y1 in V by XBOOLE_0:def 3;

        hence contradiction by A7, A26, XBOOLE_0: 3;

      end;

      assume

       A28: not thesis;

      now

        assume

         A29: Y in X;

        then

        consider Y1, Y2, Y3, Y4, Y5 such that

         A30: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 and

         A31: Y5 in Y and

         A32: not Y1 misses X by A28;

        Y5 in ( union X) by A29, A31, TARSKI:def 4;

        then Y5 in Z1 by A1, A30, A32;

        then Y5 in (X \/ Z1) by XBOOLE_0:def 3;

        then Y5 in ((X \/ Z1) \/ Z2) by XBOOLE_0:def 3;

        then Y5 in (((X \/ Z1) \/ Z2) \/ Z3) by XBOOLE_0:def 3;

        then Y meets (((X \/ Z1) \/ Z2) \/ Z3) by A31, XBOOLE_0: 3;

        then Y meets ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) by XBOOLE_1: 70;

        hence contradiction by A7, XBOOLE_1: 70;

      end;

      then Y in ((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) by A8, A6, XBOOLE_0:def 3;

      then Y in (((Z1 \/ (Z2 \/ Z3)) \/ Z4) \/ Z5) by XBOOLE_1: 4;

      then Y in ((Z1 \/ ((Z2 \/ Z3) \/ Z4)) \/ Z5) by XBOOLE_1: 4;

      then Y in (Z1 \/ (((Z2 \/ Z3) \/ Z4) \/ Z5)) by XBOOLE_1: 4;

      then Y in (((Z2 \/ Z3) \/ Z4) \/ Z5) by A9, XBOOLE_0:def 3;

      then Y in ((Z2 \/ (Z3 \/ Z4)) \/ Z5) by XBOOLE_1: 4;

      then Y in (Z2 \/ ((Z3 \/ Z4) \/ Z5)) by XBOOLE_1: 4;

      then Y in ((Z3 \/ Z4) \/ Z5) by A14, XBOOLE_0:def 3;

      then Y in (Z3 \/ (Z4 \/ Z5)) by XBOOLE_1: 4;

      then Y in (Z4 \/ Z5) by A19, XBOOLE_0:def 3;

      then Y in Z5 by A24, XBOOLE_0:def 3;

      then Y meets X by A3;

      hence contradiction by A8, A7, XBOOLE_1: 70;

    end;

    theorem :: XREGULAR:7

     not (X1 in X2 & X2 in X3 & X3 in X1)

    proof

      

       A1: X2 in {X1, X2, X3} & X3 in {X1, X2, X3} by ENUMSET1:def 1;

      

       A2: X1 in {X1, X2, X3} by ENUMSET1:def 1;

      then

      consider T be set such that

       A3: T in {X1, X2, X3} and

       A4: {X1, X2, X3} misses T by Th1;

      T = X1 or T = X2 or T = X3 by A3, ENUMSET1:def 1;

      hence thesis by A2, A1, A4, XBOOLE_0: 3;

    end;

    theorem :: XREGULAR:8

     not (X1 in X2 & X2 in X3 & X3 in X4 & X4 in X1)

    proof

      

       A1: X2 in {X1, X2, X3, X4} & X3 in {X1, X2, X3, X4} by ENUMSET1:def 2;

      

       A2: X4 in {X1, X2, X3, X4} by ENUMSET1:def 2;

      

       A3: X1 in {X1, X2, X3, X4} by ENUMSET1:def 2;

      then

      consider T be set such that

       A4: T in {X1, X2, X3, X4} and

       A5: {X1, X2, X3, X4} misses T by Th1;

      T = X1 or T = X2 or T = X3 or T = X4 by A4, ENUMSET1:def 2;

      hence thesis by A3, A1, A2, A5, XBOOLE_0: 3;

    end;

    theorem :: XREGULAR:9

     not (X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X1)

    proof

      assume that

       A1: X1 in X2 and

       A2: X2 in X3 and

       A3: X3 in X4 and

       A4: X4 in X5 and

       A5: X5 in X1;

      set Z = {X1, X2, X3, X4, X5};

      

       A6: for Y st Y in Z holds Z meets Y

      proof

        let Y such that

         A7: Y in Z;

        now

          per cases by A7, ENUMSET1:def 3;

            suppose

             A8: Y = X1;

            take y = X5;

            thus y in Z & y in Y by A5, A8, ENUMSET1:def 3;

          end;

            suppose

             A9: Y = X2;

            take y = X1;

            thus y in Z & y in Y by A1, A9, ENUMSET1:def 3;

          end;

            suppose

             A10: Y = X3;

            take y = X2;

            thus y in Z & y in Y by A2, A10, ENUMSET1:def 3;

          end;

            suppose

             A11: Y = X4;

            take y = X3;

            thus y in Z & y in Y by A3, A11, ENUMSET1:def 3;

          end;

            suppose

             A12: Y = X5;

            take y = X4;

            thus y in Z & y in Y by A4, A12, ENUMSET1:def 3;

          end;

        end;

        hence thesis by XBOOLE_0: 3;

      end;

      X1 in {X1, X2, X3, X4, X5} by ENUMSET1:def 3;

      hence contradiction by A6, Th1;

    end;

    theorem :: XREGULAR:10

     not (X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X1)

    proof

      assume that

       A1: X1 in X2 and

       A2: X2 in X3 and

       A3: X3 in X4 and

       A4: X4 in X5 and

       A5: X5 in X6 and

       A6: X6 in X1;

      set Z = {X1, X2, X3, X4, X5, X6};

      

       A7: for Y st Y in Z holds Z meets Y

      proof

        let Y such that

         A8: Y in Z;

        now

          per cases by A8, ENUMSET1:def 4;

            suppose

             A9: Y = X1;

            take y = X6;

            thus y in Z & y in Y by A6, A9, ENUMSET1:def 4;

          end;

            suppose

             A10: Y = X2;

            take y = X1;

            thus y in Z & y in Y by A1, A10, ENUMSET1:def 4;

          end;

            suppose

             A11: Y = X3;

            take y = X2;

            thus y in Z & y in Y by A2, A11, ENUMSET1:def 4;

          end;

            suppose

             A12: Y = X4;

            take y = X3;

            thus y in Z & y in Y by A3, A12, ENUMSET1:def 4;

          end;

            suppose

             A13: Y = X5;

            take y = X4;

            thus y in Z & y in Y by A4, A13, ENUMSET1:def 4;

          end;

            suppose

             A14: Y = X6;

            take y = X5;

            thus y in Z & y in Y by A5, A14, ENUMSET1:def 4;

          end;

        end;

        hence thesis by XBOOLE_0: 3;

      end;

      X1 in {X1, X2, X3, X4, X5, X6} by ENUMSET1:def 4;

      hence contradiction by A7, Th1;

    end;