XREGULAR

:: Consequences of Regularity Axiom
::  by Andrzej Trybulec
::
:: Received January 30, 2012
:: Copyright (c) 2012-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies TARSKI, XBOOLE_0;
 notations TARSKI, XBOOLE_0, ENUMSET1;
 constructors TARSKI, XBOOLE_0, ENUMSET1;
 registrations XBOOLE_0;
 requirements BOOLE;
 theorems TARSKI, XBOOLE_0, XBOOLE_1, ENUMSET1;
 schemes XFAMILY;

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;

:: To jest po prostu "poprawne" sformulowanie aksjomatu regularnosci
:: W TARSKI 'misses' jest rozekspandowane, zeby uniknac definiowania 'misses'

theorem Th1:
  ex Y st Y in X & Y misses X
proof
  consider x being 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 being object st x in X & x in Y by A3;
  hence thesis by A2,XBOOLE_0:3;
end;

theorem
  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
  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
  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
  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
  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;

:: Opuszczone dwa przypadki, ktore odpowiadaja irrefleksywnosci
:: i asymetri

theorem
  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 being 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
  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 being 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
  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
  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;