Rejestracja egzystencjalna

registration
  let x1 be Θ1;
   .....
  let xn be Θn;
  cluster ξ1 ... ξm for Θ(x1,...,xn);
  existence
  proof      :: thesis: ex x being Θ st x is ξ1 ... ξm
    take x = τ;    ::  τ -> Θ
    thus x isξ1;
      ....
    thus x is ξm
  end;
end;