Cluster Registrations

Existential Clusters

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 Clusters

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 Clusters

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;