Cluster Registrations

Existential Registrations

definition
  let X be non empty set;
  cluster non empty finite Subset of X;
  existence
  proof
    thus ex A being Subset of X st A is non empty finite;
  end;
end;

Conditional Registrations

definition
  cluster trivial -> finite set;
  coherence
  proof
    thus for A being set st A is trivial holds A is finite;
  end;
end;

definition
  let X be finite set;
  cluster -> finite Subset of X;
  coherence
  proof
    thus for A being Subset of X holds A is finite;
  end;
end;

Functorial Registrations

definition
  let X be set; let Y be non empty set;
  cluster X \/ Y -> non empty;
  coherence
  proof
    thus X \/ Y is non empty;
  end;
end;

registration
  let T be TopSpace;
  let X, Y be open Subset of T;
  cluster X \/ Y -> open Subset of T;
  coherence
  proof
    thus for R being Subset of T st R = X \/ Y holds R is open;
  end;
end;