environ

 vocabularies ENUMSET, RELATION, RELAT_AB, SETTHEOR;
 notations ENUMSET, RELATION, RELAT_AB;
 constructors ENUMSET, RELATION, RELAT_AB;
 definitions ENUMSET, RELATION, RELAT_AB;
 theorems ENUMSET, RELATION, RELAT_AB;

begin

reserve X,Y,x,y,z for set;

definition
  let x,y be set;
  pred x in y means
  not contradiction;
end;

:: definition
::   let x,y be set;
::   pred x = y means
::   not contradiction;
:: end;

theorem ax1:
  (for x holds x in X iff x in Y) implies X = Y @proof end;

definition
  let x,y be set;
  func {x,y} means :def0':
  z in it iff z=x or z=y;
  correctness @proof end;
end;

definition
  let x be set;
  func {x} means :def0:
  y in it iff y=x;
  existence
  proof
    take {x,x};
    let y;
    y in {x,x} iff y=x by def0';
    hence thesis;
  end;
  uniqueness
  proof
    let X,Y be set;
    assume a: (for z holds z in X iff z=x) & (for z being set holds z in Y iff z=x);
    now
      let z;
      thus z in X implies z in Y
      proof
        assume z in X;
        then z=x by a;
        hence thesis by a;
      end;
      thus z in Y implies z in X
      proof
        assume z in Y;
        then z=x by a;
        hence thesis by a;
      end;
    end;
    hence X=Y by ax1;
  end;
end;

scheme Separation0 { P[set] } :
  ex X being set st for x being set holds x in X iff P[x]
  @proof;
  end;

scheme Separation { A()-> set, P[set] } :
  ex X being set st for x being set holds x in X iff x in A() & P[x]
  @proof
  end;

definition
  func NotOwnElements means :def1:
  for x holds x in it iff not x in x;
  existence
  proof
    defpred P[set] means not $1 in $1;
    ex X being set st for x being set holds x in X iff P[x] from Separation0;
    hence thesis;
  end;
  uniqueness
  proof
    let X,Y be set;
    assume a: (for x being set holds x in X iff not x in x) & (for x being set holds x in Y iff not x in x);
    now
      let x being set;
      thus x in X implies x in Y
      proof
        assume x in X; then
        not x in x by a;
        hence thesis by a;
      end;
      thus x in Y implies x in X
      proof
        assume x in Y;
        then not x in x by a;
        hence thesis by a;
      end;
    end;
    hence X=Y by ax1;
  end;
end;

c1: not NotOwnElements in NotOwnElements implies NotOwnElements in NotOwnElements by def1;
c2: NotOwnElements in NotOwnElements implies not NotOwnElements in NotOwnElements by def1;

not NotOwnElements in NotOwnElements iff NotOwnElements in NotOwnElements by c1,c2;

contradiction by c1,c2;

theorem ax2:
  x in X implies ex Y st Y in X & not ex x st x in X & x in Y @proof end;

theorem l1:
  not x in x
  proof
    x: x in {x} by def0; then
    consider Y such that
    y: Y in {x} & for y st y in {x} holds not y in Y by ax2;
    n: not x in Y by x,y;
    Y = x by def0,y;
    hence thesis by n;
  end;

definition
  func AllSets means :def2:
  for x being set holds x in it;
  existence
  proof
    defpred P[set] means not contradiction;
    ex X being set st for x being set holds x in X iff P[x] from Separation0;
    hence thesis;
  end;
  uniqueness
  proof
    let X,Y be set;
    assume a: (for x being set holds x in X) & (for x being set holds x in Y);
    then for x being set holds x in X iff x in Y;
    hence X=Y by ax1;
  end;
end;

AllSets in AllSets by def2;
then contradiction by l1;

:: Barberville

reserve B for set, Goli for Relation of B,B;

definition
  let B,Goli;
  func G(B,Goli) means :defGB:
  it in B & for x st x in B holds [it,x] in Goli iff not [x,x] in Goli;
  correctness @proof end;
:: existence cannot proved!!!

end;

now
  let B,Goli;
  g: G(B,Goli) in B by defGB;
  [G(B,Goli),G(B,Goli)] in Goli iff not [G(B,Goli),G(B,Goli)] in Goli by defGB,g;
  hence contradiction;
end;