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

definition cluster trivial -> finite set;coherenceproof 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;coherenceproof thus for A being Subset of X holds A is finite; end; end;

definition let X be set; let Y be non empty set; cluster X \/ Y -> non empty;coherenceproof 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;coherenceproof thus for R being Subset of T st R = X \/ Y holds R is open; end; end;