ClosedHyperInterval (a,a) = {a} by Th48;
hence ClosedHyperInterval (a,a) is trivial ; :: thesis: verum